proposition: Lemma ball_closed (e:Q) x y: (forall d:Q, 0 < d -> ball (e+d) x y)%Q -> ball e x y.
proof: Proof. unfold ball. intro H. assert (Qle 0 e). { apply Qnot_lt_le. intro abs. destruct (H (-e*(1#2))%Q). rewrite <- (Qmult_0_l (1#2)). apply Qmult_lt_r. reflexivity. apply (Qplus_lt_l _ _ e). ring_simplify. exact abs. clear H1. ring_simplify in H0. rewrite <- (Qmult_0_r (1#2)) in H0. apply Qmult_le_l in H0. exact (Qlt_not_le _ _ abs H0). reflexivity. } split. exact H0. apply CRle_not_lt. intro abs. apply CRlt_Qmid in abs. destruct abs as [q [H1 H2]]. specialize (H (q-e)%Q). revert H2. apply CRle_not_lt. setoid_replace q with (e+(q-e))%Q by (unfold canonical_names.equiv, stdlib_rationals.Q_eq; ring). apply H. unfold Qminus. rewrite <- Qlt_minus_iff. apply Qlt_from_CRlt, H1. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.reals.fast.CRArith