Theorem: Imo2009P5.succ_pnat_add_succ_pnat (Compfiles/Imo2009P5.lean)

State before:
m n : ℕ
⊢ m.succPNat + n.succPNat = (m + n).succPNat + 1
Tactic:
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]
State after:
m n : ℕ
⊢ (m + n).succ.succ = (m + n).succ + ↑1

State before:
m n : ℕ
⊢ (m + n).succ.succ = (m + n).succ + ↑1
Tactic:
rfl
State after:
no goals