Theorem: Nat.add_sub_comm (GMLInit/Data/Nat/Sub.lean)

State before:
x y : Nat
⊢ x + (y - x) = y + (x - y)
Tactic:
rw [Nat.add_comm x, Nat.add_comm y, Nat.sub_add_eq_max, Nat.sub_add_eq_max, Nat.max_comm]
State after:
no goals