proposition: Lemma recover_sol_exists (n : nat) (Φ' : pos (n * 4) -> Z) : exists (Φ : pos n -> nat), (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); intros p; invert pos p. - destruct (IHn (fun j => Φ' (pos_right 4 j))) as [Φ H]. unshelve eexists. + intros p; invert pos p. * exact (Z.to_nat (sq (Φ' (inj3 pos0)) + sq (Φ' (inj2 pos0)) + sq (Φ' (inj1 pos0)) + sq (Φ' (inj0 pos0)))). * exact (Φ p). + intros p; invert pos p. * rewrite Z2Nat.id; auto. pose proof (Z.square_nonneg (Φ' pos3)). pose proof (Z.square_nonneg (Φ' pos2)). pose proof (Z.square_nonneg (Φ' pos1)). pose proof (Z.square_nonneg (Φ' pos0)). nia. * apply H. 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