proposition: Lemma diff_linear : forall a (p:RX), _D_ (a[+X*]p)[=]p[+]_X_[*]_D_ p.
proof: Proof. intros a p. change (p[+]([0][+X*]_D_ p)[=]p[+]_X_[*]_D_ p). rewrite -> cpoly_lin. rewrite <- c_zero. ring. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational