proposition: Lemma nrCC3_a8 : degree_le n nrCC3_poly'.
proof: Proof. replace n with (n + 0). unfold nrCC3_poly' in |- *. apply degree_le_mult. exact nrCC3_a5. apply degree_le_c_. auto with arith. Qed.
imports: CoRN.complex.CComplex Coq.Arith.Wf_nat Coq.setoid_ring.ArithRing