proposition: Lemma UniformContProper : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (cont_mod : forall x:CRcarrier R, 0 < x -> CRcarrier R), UniformCont f cont_mod -> (forall x y : CRcarrier R, x == y -> f x == f y).
proof: Proof. intros. destruct H. split. - intro abs. assert (0 < f y - f x) as epsPos. { rewrite <- (CRplus_opp_r (f x)). apply CRplus_lt_compat_r. exact abs. } specialize (c0 (f y - f x) x y epsPos). apply (CRle_abs (f y - f x)). rewrite CRabs_minus_sym. apply c0. apply (CRle_lt_trans _ (CRabs _ 0)). rewrite H0. unfold CRminus. rewrite CRplus_opp_r. apply CRle_refl. rewrite CRabs_right. apply c. apply CRle_refl. - intro abs. assert (0 < f x - f y) as epsPos. { rewrite <- (CRplus_opp_r (f y)). apply CRplus_lt_compat_r. exact abs. } specialize (c0 (f x - f y) x y epsPos). apply (CRle_abs (f x - f y)). apply c0. apply (CRle_lt_trans _ (CRabs _ 0)). rewrite H0. unfold CRminus. rewrite CRplus_opp_r. apply CRle_refl. rewrite CRabs_right. apply c. apply CRle_refl. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal