Lemma CRopp_strext : un_op_strext CRasCSetoid CRopp.

Definition CRoppasUnOp : CSetoid_un_op CRasCSetoid :=
Build_CSetoid_fun _ _ _ CRopp_strext.

Lemma CRisCGroup : is_CGroup CRasCMonoid CRoppasUnOp.

Definition CRasCGroup : CGroup :=
Build_CGroup _ _ CRisCGroup.

Canonical Structure CRasCGroup.