proposition: Lemma nrootCC_2 : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c -> z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] [0] -> z[^]n [=] c or z[^]n [=] [--]c.
proof: Proof. intros. apply cond_square_eq; try assumption. exact TwoCC_ap_zero. apply nrootCC_2'; assumption. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing