proposition: Lemma StepApproxIntegralIncr : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (s1 t1 s2 t2 : CRcarrier (RealT (ElemFunc IS))) (ltst1 : 0 < s1 < t1) (ltst2 : 0 < s2 < t2), s1 <= s2 -> t1 <= t2 -> Integral (StepApproxIntegrable f s2 t2 ltst2 fInt) <= Integral (StepApproxIntegrable f s1 t1 ltst1 fInt).
proof: Proof. intros. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, xdg. rewrite (DomainProp f x d2 d), (DomainProp f x d1 d), (DomainProp f x d0 d). generalize (partialApply f x d). intro c. rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite <- CRopp_mult_distr_l, CRmult_1_l. apply StepApproxLe; assumption. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia