proposition: Lemma cpoly_map_diff : forall p, cpoly_map (_D_ p) [=] _D_ (cpoly_map p).
proof: Proof. induction p. reflexivity. change (cpoly_map (_D_ (s[+X*]p))[=]_D_ (f s[+X*](cpoly_map p))). do 2 rewrite -> diff_linear. autorewrite with ringHomPush. rewrite -> IHp. rewrite -> cpoly_map_X. reflexivity. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational