proposition: Lemma lin_mult : forall (p q : RX) c, (c[+X*]p) [*]q [=] _C_ c[*]q[+]_X_[*] (p[*]q).
proof: Proof. intros. astepl ((_C_ c[+]_X_[*]p)[*]q). astepl (_C_ c[*]q[+]_X_[*]p[*]q). algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational