proposition: Lemma Cmult_neq_0 (z1 z2 : C) : z1 <> 0 -> z2 <> 0 -> z1 * z2 <> 0.
proof: Proof. intros Hz1 Hz2 => Hz. assert (Cmod (z1 * z2) = 0). by rewrite Hz Cmod_0. rewrite Cmod_mult in H. apply Rmult_integral in H ; destruct H. now apply Hz1, Cmod_eq_0. now apply Hz2, Cmod_eq_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy