proposition: Lemma series_cv_abs_le : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (a : CRcarrier R) (cau : CR_cauchy R (CRsum (fun n => CRabs R (un n)))), CRle R a (let (c,_) := series_cv_abs un cau in c) -> { l : CRcarrier R & prod (CRle R a l) (series_cv un l) }.
proof: Proof. intros. destruct (series_cv_abs un cau). exists x. split; assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase