proposition: Lemma m_less (m:nat) (e : env (model m)) (l r : nat) : m > 0 -> e ⊨ less l r <-> exists n1 u1 n2 u2, (e l) = Num (@fN _ n1 u1) /\ (e r) = Num (@fN _ n2 u2) /\ n1 < n2.
proof: Proof. split. - intros [[nl [ul [nr [ur [Hl [Hr Hlr]]]]]]%m_leq Hneq]. 2:easy. exists nl,ul,nr,ur. split. 2:split. 1-2:easy. enough (nl <> nr) by lia. intros Hc. cbn -[deq] in Hneq. apply Hneq. erewrite -> m_deq. 2:easy. rewrite Hl, Hr. f_equal. subst nl. f_equal. apply le_unique. - intros [nl [ul [nr [ur [Hl [Hr Hlr]]]]]]. cbn -[deq leq]. split. + apply m_leq. 1:easy. exists nl,ul,nr,ur. split. 1:easy. split. 1:easy. lia. + intros Hc. enough (nl = nr) by lia. rewrite m_deq in Hc. 2:easy. rewrite Hl,Hr in Hc. congruence. 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