Example of a abelian group: ⟨CR,+⟩



Lemma CRisCAbGroup : is_CAbGroup CRasCGroup.

Definition CRasCAbGroup : CAbGroup :=
Build_CAbGroup _ CRisCAbGroup.

Canonical Structure CRasCAbGroup.