proposition: Lemma locally_ball_norm : forall (x : V) (eps : posreal), locally x (ball_norm x eps).
proof: Proof. intros x eps. apply locally_le_locally_norm. apply locally_norm_ball_norm. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub