proposition: Lemma Cmod_inv : forall x : C, x <> 0 -> Cmod (/ x) = Rinv (Cmod x).
proof: Proof. intros x Zx. apply Rmult_eq_reg_l with (Cmod x). rewrite -Cmod_mult. rewrite Rinv_r. rewrite Cinv_r. rewrite Cmod_R. apply Rabs_R1. exact Zx. contradict Zx. now apply Cmod_eq_0. contradict Zx. now apply Cmod_eq_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy