proposition: Lemma CRplus_pos_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q), Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)).
proof: Proof. intros. apply (CRle_lt_trans _ (CRplus R x 0)). - apply CRplus_0_r. - apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R 0)). + apply CRle_refl. + apply CR_of_Q_lt. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs