proposition: Lemma nrootCC_4 : forall c, c [#] [0] -> forall n, Nat.Odd n -> {z : CC | z[^]n [=] c}.
proof: Proof. intros. pattern c in |- *. apply C_cc_ap_zero; try assumption; intros. apply nrootCC_4_ap_imag; try assumption. apply nrootCC_4_ap_real; try assumption. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing