fact: Fixpoint CRsum {R : ConstructiveReals} (f:nat -> CRcarrier R) (N:nat) : CRcarrier R := match N with | O => f 0%nat | S i => CRsum f i + f (S i) end.
imports: QArith Qabs ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveLimits