Add square theorems to iset.mm
Add square theorems to iset.mm

This is sqval through nnesq , copied without change from set.mm.
Follow up changes will be needed to get all proofs to verify.

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