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

State before:
m n : ℕ+
⊢ m + n - n = m
Tactic:
rw [← add_right_inj n, PNat.add_sub_of_lt (n.lt_add_left m), add_comm]
State after:
no goals