proposition: Lemma CSUCTrapezeBounded : forall {R : ConstructiveReals} (a b eta x : CRcarrier R) (etaPos : 0 < eta), a <= b -> (0 <= CSUCUnitTrapeze a b eta etaPos x <= 1).
proof: Proof. intros. unfold CSUCUnitTrapeze, UCUnitHeaviside. rewrite (CRinv_morph (a - (a-eta)) eta _ (inr etaPos)). rewrite (CRinv_morph (b + eta - b) eta _ (inr etaPos)). destruct (CRltLinear R). destruct (s a x (b+eta)). - apply (CRle_lt_trans _ (b+0)). rewrite CRplus_0_r. exact H. apply CRplus_lt_compat_l. exact etaPos. - rewrite CRmax_right, CRmin_left. split. + apply (CRle_trans _ (1-1)). unfold CRminus. rewrite CRplus_opp_r. apply CRle_refl. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply CRmax_lub. apply CRlt_asym, CRzero_lt_one. apply CRmin_l. + apply (CRle_trans _ (1-0)). apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply CRmax_l. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. + unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite <- CRplus_assoc, CRmult_plus_distr_r, CRinv_r. apply (CRle_trans _ (0+1)). rewrite CRplus_0_l. apply CRle_refl. apply CRplus_le_compat_r. apply (CRle_trans _ ((x-a)*0)). rewrite CRmult_0_r. apply CRle_refl. apply CRlt_asym. apply CRmult_lt_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_lt_compat_r, c. apply CRinv_0_lt_compat. exact etaPos. + apply CRmin_glb. apply CRlt_asym, CRzero_lt_one. apply (CRle_trans _ ((x-(a-eta))*0)). rewrite CRmult_0_r. apply CRle_refl. apply CRlt_asym. apply CRmult_lt_compat_l. apply (CRplus_lt_reg_r (a-eta)). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r, CRplus_0_l. apply (CRlt_trans _ a). 2: apply c. apply (CRplus_lt_reg_r eta). rewrite CRplus_assoc, CRplus_opp_l. apply CRplus_lt_compat_l. exact etaPos. apply CRinv_0_lt_compat. exact etaPos. - rewrite (CRmin_right 1 ((x - b) * CRinv R eta (inr etaPos))). split. + unfold CRminus. rewrite CRplus_comm. apply (CRle_trans _ (-(CRmax 0 ((x - b) * CRinv R eta (inr etaPos))) + CRmax 0 ((x - b)* CRinv R eta (inr etaPos)))). rewrite CRplus_opp_l. apply CRle_refl. apply CRplus_le_compat_l. apply CRmax_lub. apply CRmax_l. apply (CRle_trans _ (CRmin 1 ((x + - (a + - eta)) * CRinv R eta (inr etaPos)))). 2: apply CRmax_r. apply CRmin_glb. apply (CRmult_le_reg_r eta _ 1). exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_r, CRmult_1_l. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm. apply CRlt_asym, c. apply CRmult_le_compat_r. apply CRlt_asym, CRinv_0_lt_compat. exact etaPos. apply CRplus_le_compat_l. apply CRopp_ge_le_contravar. apply (CRplus_le_reg_r eta). rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply (CRle_trans _ (b+0)). rewrite CRplus_0_r. exact H. apply CRplus_le_compat_l. apply CRlt_asym, etaPos. + apply (CRplus_le_reg_r (CRmax 0 ((x - b) * CRinv R eta (inr etaPos)))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. apply CRmax_lub. apply (CRle_trans _ (1+0)). rewrite CRplus_0_r. apply CRlt_asym, CRzero_lt_one. apply CRplus_le_compat_l. apply CRmax_l. apply (CRle_trans _ (1+0)). rewrite CRplus_0_r. apply CRmin_l. apply CRplus_le_compat_l. apply CRmax_l. + apply (CRmult_le_reg_r eta _ 1). exact etaPos. rewrite CRmult_assoc, CRinv_l, CRmult_1_l, CRmult_1_r. apply (CRplus_le_reg_r b). unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. rewrite CRplus_comm. apply CRlt_asym, c. - unfold CRminus. rewrite CRplus_comm. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. reflexivity. - unfold CRminus. rewrite CRopp_plus_distr. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite CRopp_involutive. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal