proposition: Lemma nonneg_in_Qball_0 (x : Q) (Eq : 0 <= x) (ε : Q) : x <= ε <-> ball ε x 0.
proof: Proof. rewrite <-in_Qball. split. - intros ?. split. apply (Q.Qplus_le_r ε). now ring_simplify. apply (Qle_trans _ (x+0)). rewrite Qplus_0_r. exact Eq. apply Qplus_le_r. exact (Qle_trans _ _ _ Eq H). - intros [? ?]. apply (Q.Qplus_le_r (- ε)). rewrite Qplus_comm. now ring_simplify. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals