proposition: Lemma nrCC3_a6 : nth_coeff n nrCC3_poly'' [=] [1].
proof: Proof. cut (monic n nrCC3_poly''); intros. unfold monic in H. elim H; intros; assumption. replace n with (1 * n). unfold nrCC3_poly'' in |- *. apply monic_nexp. unfold monic in |- *; split. apply eq_reflexive_unfolded. exact nrCC3_a4. unfold mult in |- *. auto with arith. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing