proposition: Lemma lagrange_prelim p : prime p -> exists n a b, n*p = 1+a*a+b*b /\ 0 < n < p.
proof: Proof. intros Hp. destruct (prime_2_or_odd Hp) as [ | (n & Hn1 & Hn2) ]. + exists 1, 1, 0; subst; auto. + destruct (lagrange_prelim_odd _ Hp Hn2) as (a & b & (k & Hk) & Ha & Hb). exists k, a, b; split; auto. split. 1: destruct k; simpl in Hk; try lia; discriminate. assert (a <= n) as Ha' by lia. assert (b <= n) as Hb' by lia. destruct (le_lt_dec p k) as [ H | H ]; auto. exfalso. assert (a*a+2*(1*1)+b*b <= k*p) as C; try lia. apply Nat.le_trans with ((n+n)*(n+n)). 2: apply Nat.mul_le_mono; lia. rewrite remarkable_id1_nat. apply Nat.add_le_mono; [ | apply Nat.mul_le_mono; auto ]. apply Nat.add_le_mono; [ apply Nat.mul_le_mono; auto | ]. apply Nat.mul_le_mono_l. now apply Nat.mul_le_mono. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.H10.ArithLibs(Zp)