proposition: Lemma cpoly_map_pres_plus : fun_pres_plus _ _ cpoly_map_csf.
proof: Proof. unfold fun_pres_plus. apply (cpoly_double_ind0 R). intros p. change (cpoly_map_csf(p[+][0])[=]cpoly_map_csf p[+][0]). stepr (cpoly_map_csf p). 2: ring. apply csf_wd. cut (forall p: cpoly_cring R, csg_op p [0] [=] p). easy. intros. ring. reflexivity. intros p q c d H. split. apply rh_pres_plus. apply H. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational