proposition: Lemma ball_weak : forall e d (a b:X), 0 <= d -> ball e a b -> ball (e + d) a b.
proof: Proof. intros e d a b dpos B1. eapply ball_triangle. apply B1. apply ball_refl. exact dpos. Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra