feat(data/pnat/basic): add induction principle (#6410)
An induction principle for `pnat`. The proof is by Mario Carneiro. If there are mistakes, I introduced them!
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/torsion.20free/near/227748865
