proposition: Lemma aZeroS k : ~ (k << z).
proof: Proof. Proof using vTrans vSucc vPred rho' rho m fini decP Hrho. induction k as [k IH] using (well_founded_ind less_wf). intros [Hc1 Hc2]. destruct (@vpPred k) as [k' [Hk'1 Hk'2]%vpSucc]. 1-2:firstorder. eapply (IH k'). 1:easy. eapply less_leq. 1:exact Hk'1. easy. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions