proposition: Lemma cpoly_plus_commutative : forall p q, cpoly_plus_cs p q [=] cpoly_plus_cs q p.
proof: Proof. intros. pattern p, q in |- *. apply cpoly_double_sym_ind0_cs. unfold Tsymmetric in |- *. intros. algebra. intro p0. rewrite cpoly_zero_plus. rewrite cpoly_plus_zero. algebra. intros. repeat rewrite cpoly_lin_plus_lin. apply _cpoly_lin_eq_lin. split. algebra. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational