proposition: Lemma diff_plus : forall (p q:RX), _D_ (p[+]q)[=]_D_ p[+]_D_ q.
proof: Proof. induction p. reflexivity. intros [|a q]. rewrite -> cm_rht_unit_unfolded. change (cpoly_zero R) with ([0]:cpoly_cring R); algebra. change ((p[+]q)[+]cpoly_linear _ [0] (_D_ (p[+]q))[=] (p[+]cpoly_linear _ [0] (_D_ p))[+](q[+]cpoly_linear _ [0] (_D_ q))). do 3 rewrite -> poly_linear. change (st_car RX) in p, q. change (p[+]q[+](_X_[*]_D_ (p[+]q)[+]_C_ [0])[=] p[+](_X_[*]_D_ p[+]_C_ [0])[+](q[+](_X_[*]_D_ q[+]_C_ [0]))). rewrite -> (IHp q). rewrite <- c_zero. ring. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational