rw [← PNat.coe_inj, PNat.add_coe, PNat.add_coe, Nat.succPNat_coe, Nat.succPNat_coe,
    Nat.succPNat_coe, Nat.add_succ, Nat.succ_add]
m n : ℕ
⊢ m.succPNat + n.succPNat = (m + n).succPNat + 1
m n : ℕ
⊢ (m + n).succ.succ = (m + n).succ + ↑1