proposition: Lemma coeff_Sm_mult_x_ : forall (p : RX) m, nth_coeff (S m) (p[*]_X_) [=] nth_coeff m p.
proof: Proof. intros. astepl (nth_coeff (S m) (_X_[*]p)). apply coeff_Sm_x_mult. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings