proposition: Lemma IntegralOneCSUC : forall {R : ConstructiveReals}, IntegralCSUC (PartializeFunc (CRcarrier R) (CSUCUnitTrapeze 0 0 1 (CRzero_lt_one R))) OneCSUC_IS_CSUC == 1.
proof: Proof. intro R. transitivity (CR_of_Q R 1 + 0 - 0). rewrite <- (CSUCUnitTrapezeInt 0 0 1 (CRzero_lt_one R) (CRle_refl 0)). assert (-(1) <= CR_of_Q R 1). { apply (CRle_trans _ (-0)). apply CRopp_ge_le_contravar, CRlt_asym, CRzero_lt_one. rewrite CRopp_0. apply CRlt_asym, CRzero_lt_one. } rewrite (UC_integral_bound_proper (CSUCUnitTrapeze 0 0 1 (CRzero_lt_one R)) (0-1) (0+1) (-(1)) 1 _ _ _ H). apply UC_integral_extens. reflexivity. unfold CRminus. rewrite CRplus_0_l, <- CR_of_Q_opp. apply CR_of_Q_morph. reflexivity. rewrite CRplus_0_l. reflexivity. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. reflexivity. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets