proposition: Lemma rational (r: Q) (x y: M): ball r x y <-> CRball ('r) x y.
proof: Proof. Proof with auto. split... repeat intro. apply CRle_Qle in H0. apply ball_weak_le with r... intros. apply H, CRle_refl. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs