proposition: Lemma IntegralNonDecreasingAE : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), almost_everywhere (fun x : X (ElemFunc IS) => forall (dF : Domain f x) (dG : Domain g x), partialApply _ _ dF <= partialApply _ _ dG) -> Integral fInt <= Integral gInt.
proof: Proof. intros. destruct X as [h [hInt inc]]. pose proof (IntegralNonDecreasing (Xplus f (Xminus h h)) (Xplus g (Xminus h h)) (IntegrablePlus f (Xminus h h) fInt (IntegrableMinus hInt hInt)) (IntegrablePlus g (Xminus h h) gInt (IntegrableMinus hInt hInt))). rewrite IntegralPlus in H. rewrite IntegralPlus in H. rewrite IntegralMinus in H. unfold CRminus in H. rewrite CRplus_opp_r, CRplus_0_r, CRplus_0_r in H. apply H. intros x xdf xdg. destruct xdf, xdg. rewrite (applyXplus f (Xminus h h)), (applyXplus g (Xminus h h)). destruct d0, d2. rewrite (applyXminus h h), (applyXminus h h). destruct f,g,h; simpl; clear H gInt fInt. simpl in inc. rewrite (DomainProp1 _ d3 d0), (DomainProp1 _ d2 d0), (DomainProp1 _ d4 d0). unfold CRminus. rewrite CRplus_opp_r, CRplus_0_r, CRplus_0_r. apply inc. apply d2. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions