Add partial 2sq development in iset.mm (#4388)

* Add 2sqlem1 to iset.mm

Stated as in set.mm.  The proof is similar to the set.mm proof but needs
some intuitionizing.

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

* copy mul2sq from set.mm to iset.mm

* Add 2sqlem3 to iset.mm

Stated as in set.mm.  The proof needs a small amount of intuitionizing
but is only slightly changed from the set.mm proof.

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

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

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

* Add 2sqlem7 to iset.mm

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

* Add 2sqlem8a to iset.mm

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

* Add 2sqlem8 to iset.mm

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

* Add 2sqlem9 to iset.mm

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

* Add 2sqlem10 to iset.mm

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

* Adjust 2sq comments in iset.mm

Add 2sqlem11 and 2sq to mmil.html

Don't refer to 2sq in comments because we haven't proved it yet.