proposition: Lemma CSUCUnitTrapeze_cont : forall {R : ConstructiveReals} (a b eta : CRcarrier R) (etaPos : 0 < eta), a <= b -> UniformCont (CSUCUnitTrapeze a b eta etaPos) (fun eps epsPos => eps * CR_of_Q R (1#2) * eta).
proof: Proof. intros. apply (UC_modExt _ (fun eps epsPos => CRmin (eps * CR_of_Q R (1#2) * (a - (a - eta))) (eps * CR_of_Q R (1#2) * (b + eta - b)))). - apply (UC_plus _ _ (fun eps epsPos => eps * (a-(a-eta))) (fun eps epsPos => eps * (b+eta-b))). apply UCHeaviside_cont. split. intros. rewrite CRplus_comm. unfold CRminus. rewrite CRplus_assoc, CRplus_opp_r, CRplus_0_r. rewrite <- (CRmult_0_r x). apply CRmult_lt_compat_l. exact xPos. exact etaPos. intros. unfold CRminus. rewrite <- CRopp_plus_distr. rewrite CRabs_opp. apply UCHeaviside_cont. apply epsPos. apply H0. - intros. rewrite CRmin_left. unfold CRminus. rewrite CRopp_plus_distr, <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. rewrite CRopp_involutive. reflexivity. setoid_replace (a - (a - eta)) with eta. setoid_replace (b + eta - b) with eta. apply CRle_refl. 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