fact: Fixpoint nth_coeff (n : nat) (p : RX) {struct p} : R := match p with | cpoly_zero => [0] | cpoly_linear c q => match n with | O => c | S m => nth_coeff m q end end.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings