m n : Nat
x✝¹ : 0 < m + 1
x✝ : 0 < n + 1
⊢ m - n < m + 1 - 0
m n : Nat
x✝¹ : 0 < m + 1
x✝ : 0 < n + 1
⊢ m + 1 - (n + 1) < m + 1 - 0
rw [Nat.add_sub_add_right]
no goals
m n : Nat
x✝¹ : 0 < m + 1
x✝ : 0 < n + 1
⊢ m - n < m + 1 - 0
exact lt_succ_of_le (Nat.sub_le _ _)
k m n : Nat
h1 : k + 1 < m + 1
h2 : k + 1 < n + 1
⊢ m - n < m - k
k m n : Nat
h1 : k + 1 < m + 1
h2 : k + 1 < n + 1
⊢ m + 1 - (n + 1) < m + 1 - (k + 1)
rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
no goals
k m n : Nat
h1 : k + 1 < m + 1
h2 : k + 1 < n + 1
⊢ m - n < m - k
exact Nat.sub_lt_sub_left (Nat.lt_of_succ_lt_succ h1) (Nat.lt_of_succ_lt_succ h2)