proposition: Theorem lagrange_4_square_theorem : forall n, 0 <= n -> foursquare n.
proof: Proof. intros n; eapply Z_prime_rect; auto. repeat (exists 0); auto. exists 1; repeat (exists 0); auto. apply foursquare_prime. apply mult_foursquare_compat. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm Znumfacts