proposition: Lemma mult_foursquare_compat : forall n m : Z, foursquare n -> foursquare m -> foursquare (n * m)%Z.
proof: Proof. intros n m (a, (b, (c, (d, Hn)))) (x, (y, (z, (t, Hm)))); subst. rewrite euler's_identity. repeat eexists. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts