proposition: Corollary lagrange_theorem_Z n : 0 <= n <-> exists a b c d, n = a*a+b*b+c*c+d*d.
proof: Proof. split. + intros H. destruct Z_of_nat_complete with (1 := H) as (m & ->). apply lagrange_theorem_nat. + intros (a & b & c & d & ->). generalize (a*a) (b*b) (c*c) (d*d) (Z.square_nonneg a) (Z.square_nonneg b) (Z.square_nonneg c) (Z.square_nonneg d). intros; lia. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)