mathlib

a248befb - feat(data/pnat/basic): 0 < n as a fact (#11729)