proposition: Lemma norm_compat2 : forall (x y : V) (eps : posreal), ball x eps y -> norm (minus y x) < norm_factor * eps.
proof: Proof. apply: NormedModule.ax4. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub