proposition: Lemma IntegralFstNonNeg : forall { I J : IntegrationSpace } (f : PartialFunction (prod (X (ElemFunc I)) (X (ElemFunc J)))) (fInt : IntegrableFunctionAE f), nonNegFunc f -> nonNegFunc (IntegralFst f fInt).
proof: Proof. intros. intros x xdf. destruct fInt, p; simpl; simpl in xdf. apply (@IntegralNonNeg (IntegrationSpaceCast J)). intros y ydf. apply H. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile