proposition: Lemma ball_norm_center (x : V) (e : posreal) : ball_norm x e x.
proof: Proof. eapply Rle_lt_trans, e. rewrite minus_eq_zero norm_zero. by apply Req_le. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub