proposition: Lemma ball_le : forall (x : M) (e1 e2 : R), e1 <= e2 -> forall (y : M), ball x e1 y -> ball x e2 y.
proof: Proof. intros x e1 e2 H y H1. destruct H. assert (e2 - e1 > 0). by apply Rgt_minus. assert (ball y {| pos := (e2-e1); cond_pos := (H0) |} y). apply ball_center. replace e2 with (e1 + (e2 - e1)). apply ball_triangle with y ; assumption. by apply Rplus_minus. by rewrite <- H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub