proposition: Lemma mult_apply : forall (p q : RX) x, (p[*]q) ! x [=] p ! x[*]q ! x.
proof: Proof. intros. pattern p in |- *. apply cpoly_induc. astepl ([0] ! x). simpl in |- *. algebra. intros. astepl (_C_ c[*]q[+]_X_[*](p0[*]q)) ! x. astepl ((_C_ c[*]q) ! x[+](_X_[*](p0[*]q)) ! x). astepl ((_C_ c[*]q) ! x[+]([0][+]_X_[*](p0[*]q)) ! x). astepl ((_C_ c[*]q) ! x[+](_C_ [0][+]_X_[*](p0[*]q)) ! x). astepl ((_C_ c[*]q) ! x[+]([0][+X*]p0[*]q) ! x). astepl ((_C_ c[*]q) ! x[+]([0][+]x[*](p0[*]q) ! x)). astepl (c[*]q ! x[+]x[*](p0[*]q) ! x). astepl (c[*]q ! x[+]x[*](p0 ! x[*]q ! x)). astepr ((c[+]x[*]p0 ! x)[*]q ! x). astepr (c[*]q ! x[+]x[*]p0 ! x[*]q ! x). algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational