proposition: Lemma differentNums (m:nat) (base:finNum m) : m > 0 -> exists (m1 m2 : finNum m), m1 <> m2 /\ ( (model_rel (Num m1) (Num base) /\ model_rel (Num m2) (Num base)) \/(model_rel (Num base) (Num m1) /\ model_rel (Num base) (Num m2)) ).
proof: Proof. intros Hm0. destruct base as [[|n] Hn]. * eexists (@fN m 0 _). eexists (@fN m 1 _). split. - intros H. congruence. - right. cbn. lia. * eexists (@fN m 0 _). eexists (@fN m 1 _). split. - intros H. congruence. - left. cbn. lia. Unshelve. all: lia. 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