proposition: Lemma LipschitzUC : forall {R : ConstructiveReals} (f : CRcarrier R -> CRcarrier R) (k : CRcarrier R) (kPos : 0 < k), Lipschitz f k -> UniformCont f (fun eps epsPos => eps * CRinv R k (inr kPos)).
proof: Proof. split. - intros eps epsPos. apply (CRle_lt_trans _ (eps * 0)). rewrite CRmult_0_r. apply CRle_refl. apply CRmult_lt_compat_l. exact epsPos. apply CRinv_0_lt_compat, kPos. - intros. apply (CRle_lt_trans _ _ _ (H x y)). apply (CRmult_lt_compat_r k) in H0. rewrite CRmult_assoc, CRinv_l, CRmult_1_r in H0. rewrite CRmult_comm. exact H0. exact kPos. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal