proposition: Lemma c_mult_apply : forall (q : RX) c x, (_C_ c[*]q) ! x [=] c[*]q ! x.
proof: Proof. intros. astepl ((cpoly_mult_cr R q c:RX)[+]([0][+X*][0])) ! x. astepl ((cpoly_mult_cr R q c) ! x[+]([0][+X*][0]) ! x). astepl ((cpoly_mult_cr R q c) ! x[+]([0][+]x[*][0])). astepl ((cpoly_mult_cr R q c) ! x[+]([0][+][0])). astepl ((cpoly_mult_cr R q c) ! x[+][0]). astepl (cpoly_mult_cr R q c) ! x. pattern q in |- *. apply cpoly_induc. simpl in |- *. algebra. intros. astepl (c[*]c0[+X*]cpoly_mult_cr R p c) ! x. astepl (c[*]c0[+]x[*](cpoly_mult_cr R p c) ! x). astepl (c[*]c0[+]x[*](c[*]p ! x)). astepr (c[*](c0[+]x[*]p ! x)). astepr (c[*]c0[+]c[*](x[*]p ! x)). apply bin_op_wd_unfolded. algebra. astepl (x[*]c[*]p ! x). astepr (c[*]x[*]p ! x). algebra. stepr ((cpoly_mult _ (_C_ c) q)!x). apply eq_reflexive. apply apply_wd. apply eq_symmetric. apply (cpoly_mult_fast_equiv _ (_C_ c) q). apply eq_reflexive. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational