proposition: Lemma Cpow_neq_compat : forall (z : C) n, z <> C0 -> z ^ n <> C0.
proof: Proof. intros z n z_neq ; induction n. simpl ; auto with complex. simpl ; apply Cmult_integral_contrapositive_currified ; assumption. Qed.
imports: Ctacfield Cbase Cpow Lia