proposition: Lemma series_cv_abs_lt : forall {R : ConstructiveReals} (un vn : nat -> CRcarrier R) (l : CRcarrier R), (forall n:nat, CRabs R (un n) <= vn n) -> series_cv_lim_lt vn l -> series_cv_lim_lt un l.
proof: Proof. intros. destruct H0 as [x [H0 H1]]. destruct (series_cv_maj un vn x H H0) as [x0 H2]. exists x0. split. - apply H2. - apply (CRle_lt_trans _ x). + apply H2. + apply H1. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits