no goals
a b c : Nat
h : a + b ≤ c
⊢ a ≤ c - b
match le.dest h with
| ⟨d, hd⟩ =>
  apply @le.intro _ _ d
  have hd : a + d + b = c := by simp [← hd, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
  have hd := Nat.sub_eq_of_eq_add hd.symm
  exact hd.symm
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a + d = c - b
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a ≤ c - b
apply @le.intro _ _ d
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝ : a + b + d = c
hd : a + d + b = c
⊢ a + d = c - b
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a + d = c - b
have hd : a + d + b = c := by simp [← hd, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝¹ : a + b + d = c
hd✝ : a + d + b = c
hd : c - b = a + d
⊢ a + d = c - b
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝ : a + b + d = c
hd : a + d + b = c
⊢ a + d = c - b
have hd := Nat.sub_eq_of_eq_add hd.symm
no goals
a b c : Nat
h : a + b ≤ c
d : Nat
hd✝¹ : a + b + d = c
hd✝ : a + d + b = c
hd : c - b = a + d
⊢ a + d = c - b
exact hd.symm
no goals
a b c : Nat
h : a + b ≤ c
d : Nat
hd : a + b + d = c
⊢ a + d + b = c
simp [← hd, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]