proposition: Lemma StepApproxMax : forall {R : ConstructiveReals} (c s2 t2 : CRcarrier R) (ltst2 : s2 < t2), s2 <= t2 -> CRinv R (t2 - s2) (inr (CRlt_minus s2 t2 ltst2)) * (CRmin c t2 + - CRmin c s2) <= 1.
proof: Proof. intros. apply (CRmult_le_reg_l (t2-s2)). apply CRlt_minus, ltst2. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l, CRmult_1_r. apply (CRle_trans _ _ _ (CRle_abs _)). rewrite CRmin_sym, (CRmin_sym c s2). apply (CRle_trans _ _ _ (CRmin_contract _ _ _)). rewrite CRabs_right. apply CRle_refl. apply CRlt_asym, CRlt_minus, ltst2. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia