mathlib

f9b939c3 - feat(data/nat/enat): simple lemmas on `enat` (#15029)