proposition: Lemma AbsRing_norm_compat2 : forall (x y : AbsRing_NormedModuleAux) (eps : posreal), ball x eps y -> abs (minus y x) < 1 * eps.
proof: Proof. intros x y eps H. now rewrite Rmult_1_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub