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