proposition: Lemma C_NormedModule_mixin_compat2 : forall (x y : C_NormedModuleAux) (eps : posreal), ball x eps y -> Cmod (minus y x) < sqrt 2 * eps.
proof: Proof. intros x y eps H. rewrite Cmod_norm. replace (sqrt 2) with (sqrt 2 * Rmax 1 1)%R. apply: prod_norm_compat2 H. rewrite -> Rmax_left by apply Rle_refl. apply Rmult_1_r. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy