proposition: Lemma OneCSUC_IS_CSUC : forall {R : ConstructiveReals}, Is_CSUC_func (PartializeFunc (CRcarrier R) (CSUCUnitTrapeze 0 0 1 (CRzero_lt_one R))).
proof: Proof. intro R. 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. } apply (Build_Is_CSUC_func R (PartializeFunc (CRcarrier R) (CSUCUnitTrapeze 0 0 1 (CRzero_lt_one R))) (fun x:CRcarrier R => Logic.I) (-(1)) 1 H (fun eps epsPos => eps *CR_of_Q R (1#2))). pose proof (CSUCTrapeze_CSUC 0 0 1 (CRzero_lt_one R) (CRle_refl 0)). destruct H0. destruct u. split. split. intros. specialize (c0 x0 xPos). apply (CRlt_le_trans _ _ _ c0). rewrite CRmult_1_r. apply CRle_refl. intros. apply (c1 eps x0 y0 epsPos). apply (CRlt_le_trans _ _ _ H0). rewrite CRmult_1_r. apply CRle_refl. intros. apply c. destruct H0. left. apply (CRlt_le_trans _ _ _ c2). unfold CRminus. rewrite CRplus_0_l. apply CRle_refl. right. apply (CRle_lt_trans _ 1). rewrite CRplus_0_l. apply CRle_refl. exact c2. Defined.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets