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