proposition: Lemma cpoly_mult_cr_assoc_mult : forall p q c, cpoly_mult_cr_cs (cpoly_mult_cs p q) c [=] cpoly_mult_cs (cpoly_mult_cr_cs p c) q.
proof: Proof. intros. pattern p in |- *; apply cpoly_ind_cs. rewrite cpoly_zero_mult. rewrite -> cpoly_zero_mult_cr; reflexivity. intros. rewrite cpoly_lin_mult. repeat rewrite cpoly_lin_mult_cr. rewrite cpoly_lin_mult. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs (cpoly_mult_cr_cs q c0) c) (cpoly_mult_cr_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) c)). apply cpoly_mult_cr_dist. apply cpoly_plus_op_wd. apply cpoly_mult_cr_assoc_mult_cr. rewrite cpoly_lin_mult_cr. apply _cpoly_lin_eq_lin. split;algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational