proposition: Lemma Rplus_le_pos : forall {R : ConstructiveReals} (a b : CRcarrier R), 0 <= b -> a <= a + b.
proof: Proof. intros. rewrite <- (CRplus_0_r a). rewrite CRplus_assoc. apply CRplus_le_compat_l. rewrite CRplus_0_l. assumption. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits