proposition: Lemma ball_refl e: Qle 0 e -> Reflexive (ball e).
proof: Proof. unfold Reflexive, ball. intros. split. exact H. rewrite (proj1 (distance_refl x x)). apply CRle_Qle. exact H. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith