Lemma CRplus_strext : bin_op_strext CRasCSetoid (ucFun2 CRplus).

Definition CRplusasBinOp : CSetoid_bin_op CRasCSetoid :=
Build_CSetoid_bin_fun _ _ _ _ CRplus_strext.

Lemma CRisCSemiGroup : is_CSemiGroup _ CRplusasBinOp.

Definition CRasCSemiGroup : CSemiGroup :=
Build_CSemiGroup _ _ CRisCSemiGroup.

Canonical Structure CRasCSemiGroup.