proposition: Lemma locally_norm_ball : forall (x : V) (eps : posreal), locally_norm x (ball x eps).
proof: Proof. intros x eps. apply locally_norm_le_locally. apply locally_ball. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub