proposition: Lemma Markov_notnot_apart_0 : forall {R : ConstructiveReals} (x : CRcarrier R), Markov -> (~(x == 0)) -> (x ≶ 0).
proof: Proof. intros. apply CRabs_appart_0. apply CRltEpsilon, (Markov_notnot_lt_0 _ H). intro abs. contradict H0. assert (CRabs R x <= 0) as H0. { intro H0. contradict abs. apply CRltForget, H0. } pose proof (CRabs_def2 x 0 H0) as [H1 H2]. rewrite CRopp_0 in H2. split; assumption. Qed.
imports: Coq.QArith.QArith_base Coq.Reals.Abstract.ConstructiveReals Coq.Reals.Abstract.ConstructiveAbs