proposition: Lemma StepApproxProofIrrel : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (s t : CRcarrier (RealT (ElemFunc IS))) (ltst ltst2 : 0 < s < t), Integral (StepApproxIntegrable f s t ltst fInt) == Integral (StepApproxIntegrable f s t ltst2 fInt).
proof: Proof. intros. apply IntegralExtensional. intros. simpl. destruct xdf, xdg. apply (CRmult_eq_reg_l (t-s)). right. apply CRlt_minus, ltst. rewrite <- CRmult_assoc, CRinv_r, CRmult_1_l, (CRmult_comm (t-s)). apply (CRmult_eq_reg_l (t-s)). right. apply CRlt_minus, ltst. rewrite <- CRmult_assoc, <- CRmult_assoc, CRinv_r, CRmult_1_l. rewrite CRmult_comm. rewrite (DomainProp f x d2 d), (DomainProp f x d1 d). rewrite (DomainProp f x d0 d). reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia