proposition: Lemma IntAbsSumPos : forall {IS : IntegrationSpace} (fInt : @IntegralRepresentation IS), 0 <= IntAbsSum fInt.
proof: Proof. intros. destruct fInt; simpl. apply (series_cv_nonneg ((fun k : nat => Iabs (IntFn0 k) (IntFnL0 k)))). intros. apply integralPositive. intros. intros x xdf. rewrite applyXabs. apply CRabs_pos. assumption. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase