proposition: Lemma CSUCTrapezeInPlateau : forall {R : ConstructiveReals} (a b eta x : CRcarrier R) (etaPos : 0 < eta), 0 < CSUCUnitTrapeze a b eta etaPos x -> (a-eta < x < b+eta).
proof: Proof. intros. unfold CSUCUnitTrapeze in H. apply (CRplus_lt_compat_r (UCUnitHeaviside b (b + eta) (Rplus_pos_higher b eta etaPos) x)) in H. unfold CRminus in H. rewrite CRplus_0_l, CRplus_assoc, CRplus_opp_l, CRplus_0_r in H. split. - assert (0 < UCUnitHeaviside (a - eta) a (Rminus_pos_lower a eta etaPos) x). { apply (CRle_lt_trans _ (UCUnitHeaviside b (b + eta) (Rplus_pos_higher b eta etaPos) x)). 2: exact H. apply UCHeavisideBounded. } unfold UCUnitHeaviside in H0. rewrite CRmax_right in H0. apply CRlt_min in H0. destruct H0. apply (CRmult_lt_compat_r (a-(a-eta))) in c0. rewrite CRmult_0_l, CRmult_assoc, CRinv_l, CRmult_1_r in c0. rewrite <- (CRplus_opp_r (a-eta)) in c0. apply CRplus_lt_reg_r in c0. exact c0. unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite CRopp_involutive. exact etaPos. intro abs. rewrite CRmax_left in H0. exact (CRlt_asym 0 0 H0 H0). apply CRlt_asym, abs. - assert (UCUnitHeaviside b (b+eta) (Rplus_pos_higher b eta etaPos) x < 1). { apply (CRlt_le_trans _ _ _ H). apply UCHeavisideBounded. } unfold UCUnitHeaviside in H0. apply CRlt_max in H0. destruct H0 as [_ H0]. rewrite CRmin_right in H0. apply (CRmult_lt_compat_r (b+eta-b)) in H0. rewrite CRmult_1_l, CRmult_assoc, CRinv_l, CRmult_1_r in H0. apply CRplus_lt_reg_r in H0. exact H0. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. exact etaPos. intro abs. rewrite CRmin_left in H0. exact (CRlt_asym 1 1 H0 H0). apply CRlt_asym, abs. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal