Add natural numbers with min RA

Related to #324 (closed) this MR adds a resource algebra with natural numbers as the carrier and min as the operation.

The MR names the RA min_nat and uses the boxed approach suggested by @robbertkrebbers in #324 (comment 52393). I did make a small change by defining the record field with a :> such that instances of the RA coerce to nats. I'm not sure if there are any downsides to that as well, but it seemed convenient.

If this is how we decide that the min_nat RA should be implemented then the current mnat RA should be changed accordingly: renamed to max_nat, get boxed, and these breaking changes should be documented in the changelog.

Closes #324 (closed).