Port algebra/lib/mono_nat.v

## Summary

Port [`algebra/lib/mono_nat.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/lib/mono_nat.v).

> **Note:** Generalize to `MonoNumbers.lean` in the Lean port.



## Dependencies








**Rocq dependencies:**

- #261
- #231