proposition: Lemma nrCC4_a1 : {r : IR | (r[+I*][1]) [^]n[*]CC_conj c[-] (r[+I*][--][1]) [^]n[*]c [=] [0]}.
proof: Proof. elim (realpolyn_oddhaszero (nrootCC_3_poly a b n)). intro r. intro H. exists r. apply eq_transitive_unfolded with ((r[+I*][1]) [^]n[*] (a[+I*][--]b) [-] (r[+I*][--][1]) [^]n[*] (a[+I*]b)). apply eq_reflexive_unfolded. Hint Resolve nrootCC_3: algebra. apply eq_transitive_unfolded with (cc_IR (nrootCC_3_poly a b n) ! r[*] (Two[*]II)). apply eq_symmetric_unfolded. apply nrootCC_3. apply eq_transitive_unfolded with (cc_IR [0][*] (Two[*]II)). apply bin_op_wd_unfolded. apply cc_IR_wd. exact H. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with ([0][*] (Two[*]II)). apply eq_reflexive_unfolded. apply cring_mult_zero_op. unfold odd_cpoly in |- *. exists n. apply to_Codd. assumption. apply (nrootCC_3_degree a b b_ n). Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing