a b c : Nat
h : a < c - b
hle : b ≤ c
⊢ a + b < c
a b c : Nat
h : a < c - b
⊢ a + b < c
have hle : b ≤ c := by
  apply Nat.ge_of_not_lt
  intro hgt
  apply Nat.not_lt_zero a
  rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hgt)] at h
  exact h
a b c : Nat
h : a < c - b
hle : b ≤ c
this : succ a + b ≤ c
⊢ a + b < c
a b c : Nat
h : a < c - b
hle : b ≤ c
⊢ a + b < c
have : a.succ + b ≤ c := add_le_of_le_sub hle h
a b c : Nat
h : a < c - b
hle : b ≤ c
this : succ (a + b) ≤ c
⊢ a + b < c
a b c : Nat
h : a < c - b
hle : b ≤ c
this : succ a + b ≤ c
⊢ a + b < c
simp [Nat.succ_add] at this
no goals
a b c : Nat
h : a < c - b
hle : b ≤ c
this : succ (a + b) ≤ c
⊢ a + b < c
exact this
case h
a b c : Nat
h : a < c - b
⊢ ¬c < b
a b c : Nat
h : a < c - b
⊢ b ≤ c
apply Nat.ge_of_not_lt
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ False
case h
a b c : Nat
h : a < c - b
⊢ ¬c < b
intro hgt
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ a < 0
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ False
apply Nat.not_lt_zero a
case h
a b c : Nat
h : a < 0
hgt : c < b
⊢ a < 0
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ a < 0
rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hgt)] at h
no goals
case h
a b c : Nat
h : a < 0
hgt : c < b
⊢ a < 0
exact h