n k m : Nat
H : n ≤ k
h : k < n + m
this : succ k - n ≤ n + m - n
⊢ k - n < m
n k m : Nat
H : n ≤ k
h : k < n + m
⊢ k - n < m
have := Nat.sub_le_sub_right (succ_le_of_lt h) n
no goals
n k m : Nat
H : n ≤ k
h : k < n + m
this : succ k - n ≤ n + m - n
⊢ k - n < m
rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this