proposition: Lemma repr_num_isNum (f:nat -> D) (n:nat) (m:nat) : repr_nums f n -> m <= n -> isNum (f m).
proof: Proof. intros [Hzero Hrepr] Hnm. destruct m as [|m]. - rewrite Hzero. apply vF_zero. - destruct (Hrepr m Hnm) as [pl [pr [H _]]]. apply H. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.FOL.Reductions(H10UPC_to_FOL_minimal H10UPC_to_FOL_constructions) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Synthetic(Definitions) Coq(Arith Lia List)