proposition: Lemma Markov_notnot_lt : forall {R : ConstructiveReals} (x y : CRcarrier R), Markov -> (~~CRltProp R x y) -> CRltProp R x y.
proof: Proof. intros. apply CRltForget. apply (CRplus_lt_reg_r (-x)). apply (CRle_lt_trans _ 0). rewrite CRplus_opp_r. apply CRle_refl. apply CRltEpsilon. apply (Markov_notnot_lt_0 (y-x) H). intro abs. contradict H0; intro H0. contradict abs. apply CRltForget. apply (CRplus_lt_reg_r x). apply (CRle_lt_trans _ x). rewrite CRplus_0_l. apply CRle_refl. apply (CRlt_le_trans _ y). apply CRltEpsilon, H0. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRle_refl. Qed.
imports: Coq.QArith.QArith_base Coq.Reals.Abstract.ConstructiveReals Coq.Reals.Abstract.ConstructiveAbs