proposition: Lemma nrootCC_5 : forall n : nat, 0 < n -> {z : CC | z[^]n [=] c}.
proof: Proof. intros. pattern n in |- *. apply odd_double_ind. exact (nrootCC_4 c c_). exact nrCC_5a4. assumption. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing