proposition: Lemma H10_H10Z : H10 ⪯ H10Z.
proof: Proof. unshelve eexists. - intros (n & p & q). exists (n * 4). exact (dp_add (to_Z_poly p) (dp_mul (dp_cnst (-1)%Z) (to_Z_poly q))). - intros (n & p & q). simpl; split; intros [ Φ H ]; simpl in *. + destruct (create_sol Φ) as [Φ' H']. exists Φ'. rewrite <- !H'; lia. + destruct (recover_sol Φ) as [Φ' H']. exists Φ'; simpl. apply Nat2Z.inj; rewrite !H'; lia. 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