proposition: Lemma cpoly_mult_commutative : forall p q : cpoly_csetoid, cpoly_mult_cs p q [=] cpoly_mult_cs q p.
proof: Proof. intros. pattern p in |- *. apply cpoly_ind_cs. rewrite cpoly_zero_mult. apply eq_symmetric_unfolded. apply cpoly_mult_zero. intros. rewrite cpoly_lin_mult. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_linear_cs [0] (cpoly_mult_cs q p0))). 2: apply eq_symmetric_unfolded; apply cpoly_mult_lin. apply cpoly_plus_op_wd. algebra. apply cpoly_linear_wd. algebra. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational