no goals
a b c : Nat
h : a - b ≤ c
⊢ a ≤ c + b
match le.dest h, Nat.le_total a b with
| _, Or.inl hle =>
  exact Nat.le_trans hle (Nat.le_add_left ..)
| ⟨d, hd⟩, Or.inr hge =>
  apply @le.intro _ _ d
  rw [Nat.add_comm, ← Nat.add_sub_assoc hge] at hd
  have hd := Nat.eq_add_of_sub_eq (Nat.le_trans hge (Nat.le_add_left ..)) hd
  rw [Nat.add_comm, hd]
no goals
a b c : Nat
h : a - b ≤ c
x✝ : Exists fun k => a - b + k = c
hle : a ≤ b
⊢ a ≤ c + b
exact Nat.le_trans hle (Nat.le_add_left ..)
a b c : Nat
h : a - b ≤ c
d : Nat
hd : a - b + d = c
hge : b ≤ a
⊢ a + d = c + b
a b c : Nat
h : a - b ≤ c
d : Nat
hd : a - b + d = c
hge : b ≤ a
⊢ a ≤ c + b
apply @le.intro _ _ d
a b c : Nat
h : a - b ≤ c
d : Nat
hd : d + a - b = c
hge : b ≤ a
⊢ a + d = c + b
a b c : Nat
h : a - b ≤ c
d : Nat
hd : a - b + d = c
hge : b ≤ a
⊢ a + d = c + b
rw [Nat.add_comm, ← Nat.add_sub_assoc hge] at hd
a b c : Nat
h : a - b ≤ c
d : Nat
hd✝ : d + a - b = c
hge : b ≤ a
hd : d + a = c + b
⊢ a + d = c + b
a b c : Nat
h : a - b ≤ c
d : Nat
hd : d + a - b = c
hge : b ≤ a
⊢ a + d = c + b
have hd := Nat.eq_add_of_sub_eq (Nat.le_trans hge (Nat.le_add_left ..)) hd
no goals
a b c : Nat
h : a - b ≤ c
d : Nat
hd✝ : d + a - b = c
hge : b ≤ a
hd : d + a = c + b
⊢ a + d = c + b
rw [Nat.add_comm, hd]