proposition: Lemma exist_root_n : forall n z, (n > 0)%nat -> {root | root ^ n = z}.
proof: Proof. intros n z Hn. destruct (exists_principal_polar_form z) as [r [theta Hrt]]. destruct Hrt as [Hrpos [Htheta Hpol]]. rewrite Cmult_IRC_compat_l in Hpol. rewrite <- Cexp_trigo_compat in Hpol. destruct (exist_root_n_pos r n) as (root_real, Hreal); [ auto with * | | ]. apply Hn. exists ( root_real * Cexp ((0 +i theta ) / INC n))%C. rewrite Cpow_mul_distr_l. rewrite IRC_pow_compat. rewrite Hreal. rewrite <- Cexp_mult. field_simplify (INC n * ((0 +i theta) / INC n))%C. unfold Cdiv. try rewrite Cinv_1. try rewrite Cmult_1_r. apply Hpol. apply not_0_INC. intuition. Qed.
imports: Complex Cpow_plus Cpolar Cexp Cpolar