proposition: Lemma cpoly_is_CRing_old : is_CRing cpoly_cabgroup cpoly_one cpoly_mult_op.
proof: Proof. apply Build_is_CRing with cpoly_mult_assoc. exact cpoly_mult_monoid. exact cpoly_mult_commutative. exact cpoly_cr_dist. exact cpoly_cr_non_triv. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational