Add more quadratic reciprocity theorems to iset.mm (#5025)

* Add lgsquad2lem1 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a few small
changes for apart in place of not equal.

* Add lgsquad2lem2 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with very small
changes to use apartness in place of not equal.

* copy lgsquad2 from set.mm to iset.mm

* Add lgsquad3 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with some small
changes (mostly for decidability of integer equality).

* Add 2lgslem1a1 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a few small
changes for differences between set.mm and iset.mm.

* Add 2lgslem1a2 to iset.mm

Stated as in set.mm.  The proof needs a little intuitionizing but is
basically the set.mm proof.

* copy 2lgslem1a from set.mm to iset.mm

* Add 2lgslem1b to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
a small amount of intuitionizing.

* Add 2lgslem1c to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
a little bit of intuitionizing.

* copy ceqsexv2d from set.mm to iset.mm

* Add 2lgslem1 to iset.mm

Stated as in set.mm.  The proof is based on the set.mm proof and
although the intuitionizing does involve some rearrangement, it is
basically the usual changes like rational numbers for floor functions,
replacing ovex , etc.

* Add 2lgslem2 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with only a small
change needed.

* copy 2txmxeqx from set.mm to iset.mm

* Add 2lgslem1 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
a little intuitionizing for not equal versus apart.

* Add 2lgslem3b to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a few small
changes of not equal to apart.

* Add 2lgslem3c to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with changes in a
few places of not equal to apart.

* Add 2lgslem3d to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with several changes
for not equal to apart.

* Add 2lgslem3a1 and 2lgslem3b1 to iset.mm

Stated as in set.mm.  The proofs are the set.mm proof with small changes
for differences in iset.mm modulus theorems.

* Add 2lgslem3c1 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a small amount
of intuitionizing.

* Add 2lgslem3d1 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a small amount
of intuitionizing.

* Add 2lgslem3 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with some changes
around using elpri rather than elpr (to avoid the need for ovex ).

* copy 2lgs2 from set.mm to iset.mm

* Add 2lgslem4 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with a few changes
for differences in modulus theorems.

* Add 2lgs to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but one
proposition needs to be shown to be decidable and the nearby logic
is rearranged accordingly.

Author: jkingdon