proposition: Lemma AbsRing_ball_sym : forall (x y : K) (e : R), AbsRing_ball x e y -> AbsRing_ball y e x.
proof: Proof. intros x y e. by rewrite /AbsRing_ball abs_minus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub