proposition: Lemma weak_le (r r': CR): r <= r' -> forall x y, CRball r x y -> CRball r' x y.
proof: Proof. intros ??? E ??. apply E. apply CRle_trans with r'; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs