proposition: Lemma cpoly_mult_assoc : associative cpoly_mult_op.
proof: Proof. unfold associative in |- *. intros p q r. change (cpoly_mult_cs p (cpoly_mult_cs q r) [=] cpoly_mult_cs (cpoly_mult_cs p q) r) in |- *. pattern p in |- *; apply cpoly_ind_cs. repeat rewrite cpoly_zero_mult. algebra. intros. repeat rewrite cpoly_lin_mult. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cs (cpoly_mult_cr_cs q c) r) (cpoly_mult_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) r)). apply cpoly_plus_op_wd. apply cpoly_mult_cr_assoc_mult. rewrite cpoly_lin_mult. apply eq_transitive_unfolded with (cpoly_plus_cs cpoly_zero_cs (cpoly_linear_cs [0] (cpoly_mult_cs (cpoly_mult_cs p0 q) r))). rewrite cpoly_zero_plus. apply _cpoly_lin_eq_lin. split. algebra. assumption. apply cpoly_plus_op_wd. apply eq_symmetric_unfolded. apply cpoly_mult_cr_zero. apply _cpoly_lin_eq_lin. split. algebra. algebra. apply eq_symmetric_unfolded. apply cpoly_mult_dist_rht. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational