proposition: Lemma ball_norm_sym : forall (x y : V) (eps : posreal), ball_norm x eps y -> ball_norm y eps x.
proof: Proof. intros x y eps Hxy. unfold ball_norm. rewrite <- norm_opp. rewrite opp_minus. apply Hxy. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub