proposition: Lemma Markov_notnot_apart : forall {R : ConstructiveReals} (x y : CRcarrier R), Markov -> (~(x == y)) -> (x ≶ y).
proof: Proof. intros. apply (CRplus_appart_reg_r (-y)). rewrite CRplus_opp_r. apply (Markov_notnot_apart_0 _ H). intro abs. contradict H0. apply (CRplus_eq_reg_r (-y)). rewrite CRplus_opp_r. exact abs. Qed.
imports: Coq.QArith.QArith_base Coq.Reals.Abstract.ConstructiveReals Coq.Reals.Abstract.ConstructiveAbs