proposition: Lemma ball_norm_eq : forall x y : V, (forall eps : posreal, ball_norm x eps y) -> x = y.
proof: Proof. intros x y H. apply plus_reg_r with (opp x). rewrite plus_opp_r. apply eq_sym, norm_eq_zero. apply Rle_antisym. 2: apply norm_ge_0. apply prop_eps. intros eps He. exact (H (mkposreal eps He)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub