Add lt2msq to iset.mm
Add lt2msq to iset.mm

The lemma lt2msq1 is copied without change from set.mm.

The theorem lt2msq is stated as in set.mm, and the proof is also
based on ( A x. A ) <_ ( B x. B ) -> A <_ B , but needs a fair bit
of rearranging to replace lttrid with ltleap . We also replace
oveq12d with mulext .

metamath/set.mm,metamath/set.mm,metamath/set.mm