proposition: Lemma C_NormedModule_mixin_compat1 : forall (x y : C) (eps : R), Cmod (minus y x) < eps -> ball x eps y.
proof: Proof. intros x y eps. rewrite Cmod_norm. apply: prod_norm_compat1. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy