proposition: Lemma create_sol_correct E (n : nat) (Φ : pos n -> nat) (Φ' : 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 -> forall p : dionat.dio_polynomial (pos n) E, Z.of_nat (dio_single.dp_eval Φ (fun _ : E => 0) p) = dp_eval Φ' (fun _ : E => 0%Z) (to_Z_poly p).
proof: Proof. intros H p. induction p as [ k | v | | [] ]; cbn; auto. - rewrite H; ring. - rewrite Nat2Z.inj_add; congruence. - rewrite Nat2Z.inj_mul; congruence. 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