proposition: Lemma IntegralNonDecreasing : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), partialFuncLe f g -> Integral fInt <= Integral gInt.
proof: Proof. intros. pose proof (IntegralMinus g f gInt fInt) as intAdd. apply (CRplus_le_reg_r (- Integral fInt)). rewrite CRplus_opp_r, <- intAdd. clear intAdd. apply representationPositive. intros x xdf. destruct (IntegrableMinusMaj g gInt f fInt). rewrite (c x xdf (d x xdf)). destruct (d x xdf). rewrite (applyXminus g f). rewrite <- (CRplus_opp_r (partialApply f x d1)). apply CRplus_le_compat. apply H. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase