proposition: Lemma nth_coeff_p_mult_c_ : forall (p : RX) c n, nth_coeff n (p[*]_C_ c) [=] nth_coeff n p[*]c.
proof: Proof. intros. astepl (nth_coeff n (_C_ c[*]p)). astepr (c[*]nth_coeff n p). apply nth_coeff_c_mult_p. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings