proposition: Lemma cpoly_mult_monoid : is_CMonoid (Build_CSemiGroup _ _ cpoly_mult_assoc) cpoly_one.
proof: Proof. apply Build_is_CMonoid. exact cpoly_mult_one. exact cpoly_one_mult. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational