proposition: Lemma nrCC3_a5 : degree_le n nrCC3_poly''.
proof: Proof. replace n with (1 * n). unfold nrCC3_poly'' in |- *. apply degree_le_nexp. exact nrCC3_a4. unfold mult in |- *. auto with arith. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing