mathlib

8255507e - feat(data/pnat/basic): Add strong induction on pnat (#4736)

feat(data/pnat/basic): Add strong induction on pnat (#4736) I added strong induction on `pnat`. (This was from a previous PR that I am splitting.) Co-authored-by: Johan Commelin <johan@commelin.net>