proposition: Lemma nrootCC_4_ap_real : {z : CC | z[^]n [=] c}.
proof: Proof. apply nrCC4_a10. elim nrCC4_a1. intro r. intro H. elim (nrCC4_a1' (r[^]2[+][1]) (a[^]2[+]b[^]2)). intro y2. intro H0. exists (nrCC4_z r y2 H0). apply nrCC4_a9. assumption. change (r[^]2[+][1] [#] [0]) in |- *. apply pos_ap_zero. apply nrCC4_a3. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing