proposition: Lemma Cmod_norm : forall x : C, Cmod x = (@norm R_AbsRing _ x).
proof: Proof. intros [u v]. unfold Cmod. simpl. apply (f_equal2 (fun x y => sqrt (x + y))) ; rewrite /norm /= !Rmult_1_r ; apply Rsqr_abs. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy