add lgsquad to iset.mm (#5018)

* Add lgsquadlemsfi to iset.mm

This is broken out from a portion of the lgsquadlem1 proof.  Shorten
that proof using this lemma.

* Add lgsquadlem2 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof although
it needs changes in various places.

Add lemma lgsquadlemofi , taken from part of the lgsquadlem1 proof.

* Add lgsquadlem3 to iset.mm

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

* Add opabn0 to mmil.html

* copy lgsquad from set.mm to iset.mm

Also, update comments, mmil.html , and mm_100.html .

Author: jkingdon