proposition: Lemma CRabs_appart_0 : forall {R : ConstructiveReals} (x : CRcarrier R), 0 < CRabs R x -> x ≶ 0.
proof: Proof. intros. destruct (CRltLinear R). clear p. pose proof (s _ x _ H) as [pos|neg]. - right. exact pos. - left. destruct (CR_Q_dense R _ _ neg) as [q [H0 H1]]. destruct (Qlt_le_dec 0 q). + destruct (s (CR_of_Q R (-q)) x 0). * apply CR_of_Q_lt. apply (Qplus_lt_l _ _ q). ring_simplify. exact q0. * exfalso. pose proof (CRabs_def R x (CR_of_Q R q)) as [H2 _]. apply H2. -- clear H2. split. ++ apply CRlt_asym, H0. ++ rewrite <- Qopp_involutive, CR_of_Q_opp. apply CRopp_ge_le_contravar, CRlt_asym, c. -- exact H1. * exact c. + apply (CRlt_le_trans _ _ _ H0). apply CR_of_Q_le. exact q0. Qed.
imports: QArith Qabs ConstructiveReals