proposition: Lemma UC_translate : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (a : CRcarrier R) (modF : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f modF -> UniformCont (fun x:CRcarrier R => f x + a) modF.
proof: Proof. split. apply H. intros. setoid_replace (f x + a - (f y + a)) with (f x - f y). destruct H. apply (c0 _ _ _ epsPos). apply H0. unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRplus_comm, CRopp_plus_distr. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal