proposition: Lemma nrCC4_a10 : forall c, {z : CC | z[^]n [=] c or z[^]n [=] [--]c} -> {z : CC | z[^]n [=] c}.
proof: Proof. intros c0 H. elim H. intros x H0. elim H0; intro H1. exists x. assumption. exists ( [--]x). apply eq_transitive_unfolded with ( [--] (x[^]n)). apply inv_nexp_odd. assumption. apply eq_transitive_unfolded with ( [--][--]c0). apply un_op_wd_unfolded. exact H1. apply cg_inv_inv. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing