proposition: Lemma StepApproxBoundPos : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (t1 t2 b : CRcarrier (RealT (ElemFunc IS))) (let1t2 : t1 <= t2), StepApproxBound f fInt t1 t2 b let1t2 -> 0 < b.
proof: Proof. intros. destruct H. apply (CRle_lt_trans _ (Integral (StepApproxIntegrable f (t1 - ext_eta x) t1 (left_ordered x) fInt) - Integral (StepApproxIntegrable f t2 (t2 + ext_eta x) (IntExtRightPos x let1t2, right_ordered x) fInt))). 2: exact c. apply (CRplus_le_reg_r (Integral (StepApproxIntegrable f t2 (t2 + ext_eta x) (IntExtRightPos x let1t2, right_ordered x) fInt))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_0_l. clear c. apply StepApproxIntegralIncr. destruct x. simpl. apply (CRle_trans _ t1). apply CRlt_asym, left_ordered0. exact let1t2. destruct x. simpl. apply (CRle_trans _ t2). exact let1t2. apply CRlt_asym, right_ordered0. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia