a b : Int
n : Nat
h : a + ↑n = b
⊢ ↑n + a - a = ↑n
a b : Int
n : Nat
h : a + ↑n = b
⊢ b - a = ↑n
rw [← h, Int.add_comm]
no goals
a b : Int
n : Nat
h : a + ↑n = b
⊢ ↑n + a - a = ↑n
simp [Int.sub_eq_add_neg, Int.add_assoc]