fact: Definition series_cv_le_lim {R : ConstructiveReals} (x : CRcarrier R) (un : nat -> CRcarrier R) : Set := { l : CRcarrier R & prod (series_cv un l) (x <= l) }.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits