proposition: Lemma Markov_notnot_lt_0 : forall {R : ConstructiveReals} (x : CRcarrier R), Markov -> (~~CRltProp R 0 x) -> CRltProp R 0 x.
proof: Proof. intro R. assert (forall (x : CRcarrier R) (n:nat), x - CR_of_Q R (1#Pos.of_nat n) < x) as bumpDown. { intros x n. apply (CRlt_le_trans _ (x-0)). apply CRplus_lt_compat_l. apply CRopp_gt_lt_contravar, CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. } intros x markov xpos. assert (exists n:nat, Qlt 0 (let (q,_) := CR_Q_dense R _ _ (bumpDown x n) in q)). { apply markov. - intro n. destruct (CR_Q_dense R _ _ (bumpDown x n)) as [q H]. destruct (Qlt_le_dec 0 q). left. exact q0. right. apply (Qle_not_lt _ _ q0). - intro abs. contradict xpos; intro xpos. apply CRltEpsilon in xpos. contradict abs. destruct (CR_archimedean R (CRinv R x (inr xpos))) as [n H]. exists (Pos.to_nat n). destruct ( CR_Q_dense R (x - CR_of_Q R (1 # Pos.of_nat (Pos.to_nat n)))%ConstructiveReals x (bumpDown x (Pos.to_nat n))) as [q H0]. apply (lt_CR_of_Q R). refine (CRle_lt_trans _ _ _ _ (fst H0)). clear H0 q. rewrite Pos2Nat.id. apply (CRplus_le_reg_r (CR_of_Q R (1#n))). unfold CRminus. rewrite CRplus_0_l. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. apply CRlt_asym in H. apply (CRmult_le_compat_l x) in H. rewrite CRinv_r in H. apply (CRmult_le_compat_r (CR_of_Q R (1#n))) in H. rewrite CRmult_1_l, CRmult_assoc, <- CR_of_Q_mult in H. setoid_replace ((Z.pos n # 1) * (1 # n))%Q with 1%Q in H. rewrite CRmult_1_r in H. exact H. unfold Qeq; simpl. rewrite Pos.mul_1_r, Pos.mul_1_r. reflexivity. apply CR_of_Q_le; discriminate. apply CRlt_asym, xpos. } clear xpos. destruct H as [n H]. destruct (CR_Q_dense R _ _ (bumpDown x n)) as [q H0]. apply CRltForget. apply (CRlt_trans _ (CR_of_Q R q)). apply CR_of_Q_lt, H. apply H0. Qed.
imports: Coq.QArith.QArith_base Coq.Reals.Abstract.ConstructiveReals Coq.Reals.Abstract.ConstructiveAbs