 Cancellative commutative monoid

A commutative monoid is cancellative when $a+c=b+c$ implies $a=b$. Cancellation makes the natural map into its Grothendieck group injective.