Add lgseisenlem3 to iset.mm (#4999)

* Add gsumfzsubmcl to iset.mm

This is gsumsubmcl from set.mm with some changes to the hypotheses.
The proof is a new one from gsumfzval , seqclg , and various monoid
theorems.

* Add seqcaopr3g to iset.mm

This is seqcaopr3 from set.mm with set existence conditions added.  The
proof is the set.mm proof except that it uses seq1g and seqp1g in place
of seq1 and seqp1 .

* Add seqcaopr2g to iset.mm

This is seqcaopr2 from set.mm with additional set existence conditions.
The proof is the set.mm proof changed to supply set existence conditions
to various seq theorems.

* Add seqcaoprg to iset.mm

This is seqcaopr from set.mm with set existence conditions added.  The
proof is the set.mm proof with the only change being to use seqcaopr2g
in place of seqcaopr2 .

* Add gsumfzmptfidmadd to iset.mm

This is gsummptfidmadd from set.mm but where the group sum needs to be
indexed by consecutive integers.  The proof is a new one based on
gsumfzval , seqcaoprg , and various monoid theorems.

* Add gsumfzmptfidmadd2 to iset.mm

This is gsummptfidmadd2 from set.mm where the sum is indexed by
consecutive integers.  The proof is via offval2 and gsumfzmptfidmadd

* Add lgseisenlem3 to iset.mm

Stated as in set.mm.  The proof is the set.mm proof with changes for set
existence, for differences in gsum theorems, to use znidom in place
of znfld , to use apartness in place of not equal, to use rationals
rather than reals in modulus theorems, and to use znunit plus coprm
in place of drngunit .

Author: jkingdon