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

State before:
x y : Nat
⊢ x - (x - y) = y - (y - x)
Tactic:
rw [Nat.sub_sub_eq_min, Nat.sub_sub_eq_min, Nat.min_comm]
State after:
no goals