proposition: Lemma ball_infinite : forall (x y z : X) (e : Q), (forall d : Q, ~ball d x y) -> ball e x z -> (forall d : Q, ~ball d z y).
proof: Proof. intros. intro abs. apply (H (e+d)). exact (ball_triangle e d x z y H0 abs). Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra