proposition: Lemma IntegralNonNeg : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), nonNegFunc f -> 0 <= Integral fInt.
proof: Proof. intros. apply representationPositive. destruct fInt, p. intros y ydf. rewrite (c y ydf (d y ydf)). apply H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase