proposition: Lemma cpoly_is_CRing : is_CRing cpoly_cabgroup cpoly_one cpoly_mult_fast_op.
proof: Proof. assert (mult_assoc:(associative cpoly_mult_fast_op)). intros p q r. stepl (cpoly_mult_op p (cpoly_mult_op q r)). stepr (cpoly_mult_op (cpoly_mult_op p q) r). apply cpoly_mult_assoc. stepl (cpoly_mult_op (cpoly_mult_fast_op p q) r). apply eq_symmetric; apply cpoly_mult_fast_equiv. apply bin_op_wd_unfolded. apply cpoly_mult_fast_equiv. apply eq_reflexive. stepl (cpoly_mult_op p (cpoly_mult_fast_op q r)). apply eq_symmetric; apply cpoly_mult_fast_equiv. apply bin_op_wd_unfolded. apply eq_reflexive. apply cpoly_mult_fast_equiv. eapply Build_is_CRing with mult_assoc. split. intro p. stepl (cpoly_mult_op p cpoly_one). apply cpoly_mult_one. apply eq_symmetric; apply cpoly_mult_fast_equiv. intro p. stepl (cpoly_mult_op cpoly_one p). apply cpoly_one_mult. apply eq_symmetric; apply cpoly_mult_fast_equiv. intros p q. stepl (cpoly_mult_op p q). stepr (cpoly_mult_op q p). apply cpoly_mult_commutative. apply eq_symmetric; apply cpoly_mult_fast_equiv. apply eq_symmetric; apply cpoly_mult_fast_equiv. intros p q r. stepl (cpoly_mult_op p (q[+]r)). stepr (cpoly_plus_op (cpoly_mult_op p q) (cpoly_mult_op p r)). apply cpoly_cr_dist. apply bin_op_wd_unfolded; apply eq_symmetric; apply cpoly_mult_fast_equiv. apply eq_symmetric; apply cpoly_mult_fast_equiv. exact cpoly_cr_non_triv. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational