proposition: Lemma cpoly_cm_proof : is_CMonoid cpoly_csemi_grp cpoly_zero.
proof: Proof. apply Build_is_CMonoid. intro; rewrite -> cpoly_plus_zero;algebra. intro x. eapply eq_transitive_unfolded. apply cpoly_plus_commutative. rewrite cpoly_plus_zero;algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational