proposition: Lemma Cmod_div (x y : C) : y <> 0 -> Cmod (x / y) = Rdiv (Cmod x) (Cmod y).
proof: Proof. move => Hy. rewrite /Cdiv. rewrite Cmod_mult. by rewrite Cmod_inv. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy