proposition: Lemma cpoly_map_apply : forall p x, f (p ! x)[=] (cpoly_map p) ! (f x).
proof: Proof. induction p. intros x. apply rh_pres_zero. intros x. simpl in *. rewrite -> rh_pres_plus. rewrite -> rh_pres_mult. rewrite -> IHp. reflexivity. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational