proposition: Lemma nrCC4_a1' : {y2 : IR | (y2[*]r2') [^]n [=] c2}.
proof: Proof. elim (realpolyn_oddhaszero (nrootCC_3'_poly c2 n)). intro y2r2'. intros. exists (y2r2'[/] r2'[//]r2'_). apply eq_transitive_unfolded with (y2r2'[^]n). apply un_op_wd_unfolded. apply div_1. apply eq_transitive_unfolded with (y2r2'[^]n[+][0]). apply eq_symmetric_unfolded. apply cm_rht_unit_unfolded. apply eq_transitive_unfolded with (y2r2'[^]n[+] ( [--]c2[+]c2)). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply cg_lft_inv_unfolded. apply eq_transitive_unfolded with (y2r2'[^]n[+][--]c2[+]c2). apply plus_assoc_unfolded. apply eq_transitive_unfolded with (y2r2'[^]n[-]c2[+]c2). apply eq_reflexive_unfolded. Hint Resolve nrootCC_3': algebra. apply eq_transitive_unfolded with ((nrootCC_3'_poly c2 n) ! y2r2'[+]c2). apply bin_op_wd_unfolded. apply eq_symmetric_unfolded. apply nrootCC_3'. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ([0][+]c2). apply bin_op_wd_unfolded. assumption. apply eq_reflexive_unfolded. apply cm_lft_unit_unfolded. unfold odd_cpoly in |- *. exists n. apply to_Codd. assumption. apply nrootCC_3'_degree. destruct n_ as [k ->]; rewrite Nat.add_1_r; exact (Nat.lt_0_succ _). Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing