proposition: Lemma m_leq (m:nat) (e : env (model m)) (l r : nat) : m > 0 -> e ⊨ leq 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 Hl]]%m_N [nr [ur Hr]]%m_N]Hlr]. exists nl,ul,nr,ur. split. 2:split. 1-2:easy. cbn in Hlr. rewrite Hl, Hr in Hlr. easy. - intros [nl [ul [nr [ur [Hl [Hr Hlr]]]]]]. cbn -[model_rel]. rewrite Hl, Hr. cbn. repeat split; 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