proposition: Lemma create_sol_exists (n : nat) (Φ : pos n -> nat) : exists (Φ' : pos (n * 4) -> Z), (forall i : pos n, Z.of_nat (Φ i) = sq (Φ' (inj3 i)) + sq (Φ' (inj2 i)) + sq (Φ' (inj1 i)) + sq (Φ' (inj0 i)))%Z.
proof: Proof. induction n as [ | n IHn ]. - exists (fun _ => 0%Z); intros p; invert pos p. - destruct (IHn (fun j => Φ (pos_nxt j))) as [Φ' H']. cbn [mult]. destruct (lagrange_theorem_nat (Φ pos0)) as (a & b & c & d & Hl). exists (fun j : pos (4 + n * 4) => match pos_both _ _ j with | inl pos0 => a | inl pos1 => b | inl pos2 => c | inl _ => d | inr j => Φ' j end). intros p; invert pos p; auto. rewrite Hl; ring. Qed.
imports: Arith ZArith Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime php utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.H10.ArithLibs(Zp lagrange) Undecidability.H10.Dio(dio_logic dio_single) Undecidability.H10(H10 H10_undec) Undecidability.H10(H10Z) Undecidability.H10.ArithLibs(Zp lagrange) Undecidability.Synthetic.Definitions