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 <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib