proposition: Lemma lagrange_prime : exists a b c d, Z.of_nat p = (a*a+b*b+c*c+d*d)%Z.
proof: Proof. Proof using Hp. replace p with (1*p) by lia; change (P 1). destruct (lagrange_prelim Hp) as (n & a & b & H1 & H2 & H3). cut (P n). + revert H2 H3; clear H1. induction on n as IH with measure n. intros H2 H3 H. destruct (le_lt_dec n 1) as [ | Hn ]. * now replace 1 with n by lia. * destruct lagrange_prime_step with (2 := H) as (m & H4 & H5); auto. generalize H5; destruct H5; apply IH; auto; lia. + exists 0%Z, 1%Z, (Z.of_nat a), (Z.of_nat b). rewrite H1, !Nat2Z.inj_add, !Nat2Z.inj_mul. simpl Z.of_nat at 1; 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)