proposition: Lemma UCmax : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (m : CRcarrier R) (fMod : forall eps:CRcarrier R, 0 < eps -> CRcarrier R), 0 <= m -> UniformCont f fMod -> UniformCont (fun x => CRmax m (f x)) fMod.
proof: Proof. intros R f m fMod mPos H. destruct H. split. exact c. intros. apply (CRle_lt_trans _ (CRabs _ (f x - f y))). 2: apply (c0 eps _ _ epsPos H). rewrite CRmax_sym, (CRmax_sym m). apply CRmax_contract. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal