m n k l : ℕ
hab : m < n
hcd : k < l
⊢ m + (k + 1) < n + l
m n k l : ℕ
hab : m < n
hcd : k < l
⊢ m + k + 1 < n + l
rw [add_assoc]
no goals
m n k l : ℕ
hab : m < n
hcd : k < l
⊢ m + (k + 1) < n + l
exact add_lt_add_of_lt_of_le hab (Nat.succ_le_iff.2 hcd)