proposition: Lemma as_distance_bound (r x y: CR): CRball r x y <-> CRdistance x y <= r.
proof: Proof. Proof with auto. unfold CRball. rewrite <- CRdistance_CRle. assert ((forall x0 : Q, r <= ' x0 -> x - ' x0 <= y /\ y <= x + ' x0) <-> x - r <= y /\ y <= x + r). split; intros. - split. + apply CRplus_le_l with (r - y). CRring_replace (r - y + (x - r)) (x - y). CRring_replace (r - y + y) r. apply (proj1 (Qle_CRle_r _ _)). intros. apply CRplus_le_l with (y - ' y'). CRring_replace (y - 'y' + (x - y)) (x - 'y'). CRring_replace (y - 'y' + 'y') y. now apply (H y'). + apply CRplus_le_r with (-x). CRring_replace (x + r - x) r. apply (proj1 (Qle_CRle_r _ _)). intros. apply CRplus_le_l with x. CRring_replace (x + (y - x)) y... apply H... - split. apply CRle_trans with (x - r). apply CRplus_le_compat... apply CRle_refl. apply -> CRle_opp... apply H. apply CRle_trans with (x + r). apply H. apply CRplus_le_compat... apply CRle_refl. - split. intros. destruct H. apply H. intros; rewrite in_CRgball; intuition. intros. destruct H. rewrite <- in_CRgball. apply H2; assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.Qabs CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs