proposition: Lemma create_sol (n : nat) (Φ : pos n -> nat) : exists Φ' : pos (n * 4) -> Z, forall p : dionat.dio_polynomial (pos n) (pos 0), Z.of_nat (dio_single.dp_eval Φ (fun _ => 0) p) = dp_eval Φ' (fun _ => 0%Z) (to_Z_poly p).
proof: Proof. destruct (create_sol_exists Φ) as [Φ']. exists Φ'; intro; now eapply create_sol_correct. 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