proposition: Lemma cpoly_map_compose : forall R S T (g:RingHom S T) (f:RingHom R S) p, (cpoly_map (RHcompose _ _ _ g f) p)[=]cpoly_map g (cpoly_map f p).
proof: Proof. induction p. constructor. split. reflexivity. apply IHp. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational