mathlib3

172bf281 - feat(data/pnat/basic): pnat is a well-order (#18700)