proposition: Lemma cpoly_map_pres_mult : fun_pres_mult _ _ cpoly_map_csf.
proof: Proof. unfold fun_pres_mult. assert (X:forall x y, cpoly_map_csf (cpoly_mult_cr _ x y)[=]cpoly_mult_cr _ (cpoly_map_csf x) (f y)). induction x; intros y. apply eq_reflexive. split. apply rh_pres_mult. apply IHx. apply (cpoly_double_ind0 R). intros p. apply eq_reflexive. intros p. change (st_car RX) in p. change (cpoly_zero R) with ([0]:RX). stepl (cpoly_map_csf ([0]:RX)). change (cpoly_map_csf [0]) with ([0]:SX). ring. apply csf_wd; ring. intros p q c d H. split. autorewrite with ringHomPush. reflexivity. change (st_car RX) in p,q. change (cpoly_map_csf ((cpoly_mult_cr _ q c)[+](p[*](cpoly_linear _ d q))) [=](cpoly_mult_cr _ (cpoly_map_csf q) (f c))[+](cpoly_map_csf p)[*](cpoly_map_csf (cpoly_linear _ d q))). stepl ((cpoly_map_csf (cpoly_mult_cr R q c))[+](cpoly_map_csf (p[*]cpoly_linear R d q))); [| apply eq_symmetric; apply cpoly_map_pres_plus]. apply csbf_wd. apply X. stepl (cpoly_map_csf ((cpoly_linear R d q:RX)[*]p)); [| apply csf_wd;ring]. stepr (cpoly_map_csf (cpoly_linear R d q)[*]cpoly_map_csf p). 2:apply (mult_commut_unfolded SX). change ((cpoly_linear R d q:RX)[*]p) with (cpoly_mult_fast_cs _ (cpoly_linear R d q) p). rewrite -> cpoly_mult_fast_equiv. rewrite cpoly_lin_mult. change (cpoly_map_csf (cpoly_linear R d q:RX)[*]cpoly_map_csf p) with (cpoly_mult_fast_cs _ (cpoly_linear S (f d) (cpoly_map_csf q)) (cpoly_map_csf p)). rewrite -> cpoly_mult_fast_equiv. rewrite cpoly_lin_mult. stepl (cpoly_map_csf (cpoly_mult_cr_cs R p d)[+]cpoly_map_csf (cpoly_linear R [0] (cpoly_mult_cs R q p))); [| apply eq_symmetric; apply cpoly_map_pres_plus]. change (cpoly_map_fun (cpoly_mult_cr_cs R p d)[+] cpoly_map_fun ([0][+X*] (cpoly_mult_cs R q p))[=] (cpoly_mult_cr_cs S (cpoly_map_fun p) (f d))[+] ([0][+X*](cpoly_mult_cs S (cpoly_map_fun q) (cpoly_map_fun p)))). apply csbf_wd. apply X. split. auto with *. change ((cpoly_map_csf (cpoly_mult_cs R q p))[=](cpoly_mult_cs S (cpoly_map_csf q) (cpoly_map_csf p))). repeat setoid_rewrite <- cpoly_mult_fast_equiv. change (cpoly_map_csf (q[*]p)[=]cpoly_map_csf q[*]cpoly_map_csf p). stepr (cpoly_map_csf p[*]cpoly_map_csf q). 2: ring. rewrite <- H. apply csf_wd;ring. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational