proposition: Lemma nrootCC_4_ap_imag : {z : CC | z[^]n [=] a[+I*]b}.
proof: Proof. elim nrootCC_4_ap_real'. intro z'. intro H. exists (z'[*]nroot_minus_I n n_). apply eq_transitive_unfolded with (z'[^]n[*]nroot_minus_I n n_[^]n). apply mult_nexp. Hint Resolve nroot_minus_I_nexp: algebra. apply eq_transitive_unfolded with ((a'[+I*]b') [*][--]II). apply bin_op_wd_unfolded. exact H. apply nroot_minus_I_nexp. apply eq_transitive_unfolded with ((a[+I*]b) [*]II[*][--]II). apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ((a[+I*]b) [*] (II[*][--]II)). apply eq_symmetric_unfolded. apply mult_assoc_unfolded. apply eq_transitive_unfolded with ((a[+I*]b) [*][1]). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. exact I_recip_rht. apply mult_one. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing