mathlib3

72eaefff - feat(data/pnat/basic): add lemmas, move `equiv.pnat_equiv_nat` (#15508)

feat(data/pnat/basic): add lemmas, move `equiv.pnat_equiv_nat` (#15508) * Add lemmas about `pnat.nat_pred` and `nat.succ_pnat`. * Use `derive` for `pnat.linear_order`. * Move `equiv.pnat_equiv_nat` to `data/pnat/basic`. * Use it in `order_iso.pnat_iso_nat` (renamed from `pnat.succ_order_iso`, swaped LHS with RHS). * Golf some proofs.