Lemma O_as_rht_unit : is_rht_unit (S:=nat_as_CSetoid) plus_is_bin_fun 0.
Lemma O_as_lft_unit : is_lft_unit (S:=nat_as_CSetoid) plus_is_bin_fun 0.
Definition nat_is_CMonoid := Build_is_CMonoid
nat_as_CSemiGroup _ O_as_rht_unit O_as_lft_unit.
Whence we can define the monoid of natural numbers:
Definition nat_as_CMonoid := Build_CMonoid nat_as_CSemiGroup _ nat_is_CMonoid.
Canonical Structure nat_as_CMonoid.
Lemma SO_as_rht_unit : is_rht_unit (S:=nat_as_CSetoid) mult_as_bin_fun 1.
Lemma SO_as_lft_unit : is_lft_unit (S:=nat_as_CSetoid) mult_as_bin_fun 1.
Definition Nmult_is_CMonoid := Build_is_CMonoid
Nmult_as_CSemiGroup _ SO_as_rht_unit SO_as_lft_unit.
Definition Nmult_as_CMonoid := Build_CMonoid Nmult_as_CSemiGroup _ Nmult_is_CMonoid.