proposition: Lemma diff_c_mult : forall c (p:RX), _D_ (_C_ c[*]p)[=]_C_ c[*]_D_ p.
proof: Proof. intros c p. induction p. auto with *. change (_D_ (cpoly_linear R s p)) with (p[+]([0][+X*](_D_ p))). change (cpoly_linear R s p) with (s[+X*]p). rewrite -> c_mult_lin. change (_D_ (c[*]s[+X*]_C_ c[*]p)) with (_C_ c[*]p [+] ([0][+X*](_D_ (_C_ c[*]p)))). rewrite -> IHp. do 2 rewrite -> cpoly_lin. rewrite <- c_zero. change (@st_eq RX (@csg_op RX (@cr_mult RX (polyconst R c) p) (@csg_op RX (cm_unit RX) (@cr_mult RX (cpoly_var R) (@cr_mult RX (polyconst R c) (cpolyder p))))) (@cr_mult RX (polyconst R c) (@csg_op RX p (@csg_op RX (cm_unit RX) (@cr_mult RX (cpoly_var R) (cpolyder p)))))). ring. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational