proposition: Lemma coeff_Sm_x_mult : forall (p : RX) m, nth_coeff (S m) (_X_[*]p) [=] nth_coeff m p.
proof: Proof. intros. astepl (nth_coeff (S m) ([0][+]_X_[*]p)). astepl (nth_coeff (S m) (_C_ [0][+]_X_[*]p)). astepl (nth_coeff (S m) ([0][+X*]p)). simpl in |- *. algebra. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings