proposition: Lemma nrootCC_3'_degree : degree n nrootCC_3'_poly.
proof: Proof. unfold nrootCC_3'_poly in |- *. apply (degree_minus_lft _ (_C_ c) (_X_[^]n) 0 n). apply degree_le_c_. pattern n at 1 in |- *; replace n with (1 * n). apply degree_nexp. apply degree_x_. replace (1 * n) with n; [auto|..]. unfold mult in |- *. auto with arith. assumption. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing