proposition: Lemma diff_mult : forall (p q:RX), _D_ (p[*]q)[=]_D_ p[*]q [+] p[*]_D_ q.
proof: Proof. induction p. intros q. change (_D_([0][*]q)[=][0][*]q[+][0][*]_D_ q). stepl (_D_([0]:RX)). 2: now destruct q. rewrite -> diff_zero. ring. intros q. change (st_car RX) in p. change (_D_((s[+X*]p)[*]q)[=]_D_(s[+X*]p)[*]q[+](s[+X*]p)[*]_D_ q). do 2 rewrite -> lin_mult. rewrite -> diff_linear. rewrite -> diff_plus. setoid_replace (_D_ ((_C_ s:RX)[*]q)) with (_C_ s[*]_D_ q) by apply diff_c_mult. setoid_replace (((_X_:RX)[*](p[*]q)):RX) with ((((_X_:RX)[*](p[*]q)))[+][0]) by (symmetry;apply cm_rht_unit_unfolded). setoid_replace ([0]:RX) with (_C_ [0]:RX) by apply c_zero. rewrite <- poly_linear. change (_D_ (cpoly_linear R [0] (p[*]q))) with (p[*]q [+] ([0][+X*]_D_ (p[*]q))). rewrite -> cpoly_lin. rewrite <- c_zero. rewrite -> IHp. ring. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational