proposition: Lemma UC_ext : forall {R : ConstructiveReals} (f g : CRcarrier R -> CRcarrier R) (modF : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f modF -> (forall x:CRcarrier R, f x == g x) -> UniformCont g modF.
proof: Proof. intros. destruct H. split. - apply c. - intros. do 2 rewrite <- H0. exact (c0 eps x y epsPos H). Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal