proposition: Lemma UC_modExt : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (modF modG : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f modF -> (forall x xPos, modF x xPos == modG x xPos) -> UniformCont f modG.
proof: Proof. split. - intros. rewrite <- H0. destruct H. apply c. - intros. rewrite <- H0 in H1. destruct H. apply (c0 _ _ _ epsPos). apply H1. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal