add lgseisen and lgsquadlem1 to iset.mm (#5014)

* Add lgseisen to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but needs
intuitionizing in a variety of ways in a number of places.

* copy relopabiv from set.mm to iset.mm

The only change is to the comment to reflect differences in the axioms.

* copy relopabv from set.mm to iset.mm

The only change is to the comment, to reflect differences in the axioms.

* Add opabidw to iset.mm

Stated as in set.mm (including the same distinct variables).  The proof,
however, just uses opabid because the set.mm proof is not easily
adapted.

* copy opelopabgf from set.mm to iset.mm

* Add opabfi to iset.mm

This is a variation of ssfidc but designed to be more specific when used
with an ordered pair abstraction.

* Add lgsquadlem1 to iset.mm

Stated as in set.mm.  The proof is basically the set.mm proof but
various places need changes for decidability, modulus theorems, and
other differences.

* fix opabidw comment

Author: jkingdon