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