proposition: Lemma Cpow_inv : forall (z : C) n, z <> C0 -> /(z ^ n) = (/z) ^ n.
proof: Proof. intros z n z_neq ; induction n. repeat (rewrite Cpow_0) ; CusingR_f. simpl ; rewrite Cinv_mult_distr ; [| assumption |]. rewrite <- IHn ; reflexivity. clear -z_neq ; induction n. simpl ; intuition (auto with complex). simpl ; apply Cmult_integral_contrapositive ; split ; assumption. Qed.
imports: Ctacfield Cbase Cpow Lia