Lemma CRmult_strext : bin_op_strext CRasCSetoid CRmult.

Definition CRmultasBinOp : CSetoid_bin_op CRasCSetoid :=
Build_CSetoid_bin_fun _ _ _ _ CRmult_strext.

Lemma CRmultAssoc : associative CRmultasBinOp.

Lemma CRisCRing : is_CRing CRasCAbGroup (' 1)%CR CRmultasBinOp.

Definition CRasCRing : CRing :=
Build_CRing _ _ _ CRisCRing.

Canonical Structure CRasCRing.