m n : Nat
h : m < n
⊢ 0 + m < n - m + m
m n : Nat
h : m < n
⊢ 0 < n - m
apply Nat.lt_of_add_lt_add_right (b := m)
no goals
m n : Nat
h : m < n
⊢ 0 + m < n - m + m
rwa [Nat.zero_add, Nat.sub_add_cancel (Nat.le_of_lt h)]