no goals
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
⊢ a + b ≤ c
match le.dest h with
| ⟨d, hd⟩ =>
  apply @le.intro _ _ d
  rw [Nat.eq_add_of_sub_eq hle hd.symm]
  simp [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = c
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b ≤ c
apply @le.intro _ _ d
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = a + d + b
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = c
rw [Nat.eq_add_of_sub_eq hle hd.symm]
no goals
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = a + d + b
simp [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]