Examples of monoids: ⟨CR,+⟩

⟨CR,+⟩

We use the addition ' 0 as the unit of monoid:

Lemma CRisCMonoid : is_CMonoid CRasCSemiGroup (' 0)%CR.

Definition CRasCMonoid : CMonoid :=
Build_CMonoid _ _ CRisCMonoid.

Canonical Structure CRasCMonoid.