proposition: Lemma AbsRing_ball_center : forall (x : K) (e : posreal), AbsRing_ball x e x.
proof: Proof. intros x e. rewrite /AbsRing_ball /minus plus_opp_r abs_zero. apply cond_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub