proposition: Lemma ball_weak_le : forall (e d:Q) (a b:X), e <= d -> ball e a b -> ball d a b.
proof: Proof. intros e d a b Hed B1. setoid_replace d with (e + (d-e)) by ring. apply (ball_triangle _ _ _ b). exact B1. apply ball_refl. unfold Qminus. rewrite <- Qle_minus_iff. exact Hed. Qed.
imports: Coq.QArith.QArith CoRN.algebra.RSetoid MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra