Because addition is associative, the natural numbers form a CSemiGroup.
Definition nat_as_CSemiGroup := Build_CSemiGroup _ plus_is_bin_fun plus_is_assoc.
Canonical Structure nat_as_CSemiGroup.
Lemma Nmult_is_CSemiGroup : is_CSemiGroup nat_as_CSetoid mult_as_bin_fun.
Definition Nmult_as_CSemiGroup := Build_CSemiGroup
nat_as_CSetoid mult_as_bin_fun Nmult_is_CSemiGroup.