proposition: Lemma ball_norm_le : forall (x : V) (e1 e2 : posreal), e1 <= e2 -> forall y, ball_norm x e1 y -> ball_norm x e2 y.
proof: Proof. intros x e1 e2 He y H1. now apply Rlt_le_trans with e1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub