proposition: Lemma nrCC_5a4 : forall n, 0 < n -> {z : CC | z[^]n [=] c} -> {z : CC | z[^]Nat.double n [=] c}.
proof: Proof. intros n H H0. elim H0. intros x H1. elim (nrootCC_1 x). intros x0 H2. exists x0. apply eq_transitive_unfolded with ((x0[^]2) [^]n). apply eq_symmetric_unfolded. apply nrCC_5a3. apply eq_transitive_unfolded with (x[^]n). apply un_op_wd_unfolded. exact H2. exact H1. apply (cs_un_op_strext _ (nexp_op (R:=CC) n)). apply ap_wdl_unfolded with c. 2: apply eq_symmetric_unfolded. 2: exact H1. apply ap_wdr_unfolded with ([0]:CC). exact c_. apply eq_symmetric_unfolded. apply zero_nexp. exact H. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing