proposition: Lemma CSUCTrapeze_CSUC : forall {R : ConstructiveReals} (a b eta : CRcarrier R) (etaPos : 0 < eta), a <= b -> CSUC (CSUCUnitTrapeze a b eta etaPos) (a-eta) (b+eta) (fun eps epsPos => eps * CR_of_Q R (1#2) * eta).
proof: Proof. intros. split. - apply CSUCUnitTrapeze_cont. apply H. - intros. unfold CSUCUnitTrapeze, UCUnitHeaviside. rewrite (CRinv_morph (a - (a-eta)) eta _ (inr etaPos)). rewrite (CRinv_morph (b + eta - b) eta _ (inr etaPos)). destruct H0 as [H0|H0]. + assert (x < a). { apply (CRlt_trans x (a-eta)). apply H0. apply Rminus_pos_lower. exact etaPos. } assert (x < b). { exact (CRlt_le_trans x a _ H1 H). } rewrite CRmax_left, CRmax_left. unfold CRminus. rewrite CRplus_opp_r. reflexivity. apply (CRle_trans _ _ _ (CRmin_r _ _)). apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_0_r. apply CRlt_asym, H2. apply (CRle_trans _ _ _ (CRmin_r _ _)). apply (CRmult_le_reg_r eta). exact etaPos. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r (a-eta)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_l, CRplus_0_r. apply CRlt_asym, H0. + assert (b < x). { apply (CRlt_trans b (b+eta)). apply Rplus_pos_higher. exact etaPos. apply H0. } assert (a < x). { exact (CRle_lt_trans a b _ H H1). } rewrite CRmax_right, CRmax_right. rewrite CRmin_left, CRmin_left. unfold CRminus. apply CRplus_opp_r. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm. apply CRlt_asym, H0. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r (a-eta)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_comm. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRlt_asym, H2. apply CRmin_glb. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_0_l. apply CRlt_asym, H1. apply CRmin_glb. apply CRlt_asym, CRzero_lt_one. apply (CRmult_le_reg_r eta _ _ etaPos). rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r. apply (CRplus_le_reg_r (a-eta)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_0_l. apply (CRle_trans _ a). 2: apply CRlt_asym, H2. apply (CRplus_le_reg_r eta). rewrite CRplus_assoc, CRplus_opp_l. apply CRplus_le_compat_l. apply CRlt_asym, etaPos. + unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. + unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal