proposition: Lemma cpoly_lin : forall (p : RX) (c : R), c[+X*]p [=] _C_ c[+]_X_[*]p.
proof: Proof. intros. astepr (c[+X*][0][+] ((cpoly_mult_cr_cs _ p [0]:RX) [+] (cpoly_linear _ ([0]:R) (cpoly_mult_cs _ (cpoly_one R) (p:cpoly_csetoid R)) :cpoly_csetoid R))). cut (cpoly_mult_cr_cs R p [0] [=] ([0]:RX)). intro. astepr (c[+X*][0][+] (([0]:RX) [+] (cpoly_linear _ ([0]:R) (cpoly_mult_cs _ (cpoly_one R) (p:cpoly_csetoid R)) :cpoly_csetoid R))). 2: apply (cpoly_mult_cr_zero R p). cut ((cpoly_mult_cs _ (cpoly_one R) (p:cpoly_csetoid R):cpoly_csetoid R) [=] p). intro. apply eq_transitive_unfolded with (c[+X*][0][+](([0]:RX) [+]cpoly_linear _ ([0]:R) (p:cpoly_csetoid R))). 2: apply bin_op_wd_unfolded. 2: algebra. 2: apply bin_op_wd_unfolded. 2: algebra. 2: apply (cpoly_linear_wd R). 2: algebra. 2: apply eq_symmetric_unfolded. 2: apply cpoly_one_mult. astepr (c[+X*][0][+]cpoly_linear _ ([0]:R) (p:cpoly_csetoid R)). astepr (c[+][0][+X*]([0][+]p)). astepr (c[+X*]p). algebra. apply cpoly_one_mult. destruct p. simpl. algebra. simpl. split. auto with *. apply eq_reflexive with (S:=cpoly_cring R). Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational