proposition: Lemma Cpow_nz (c:C) n : c <> 0 -> c^n <> 0.
proof: Proof. induction n; simpl; intro H. - injection. apply R1_neq_R0. - apply Cmult_neq_0; auto. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy