have : compare (n + k) (m + j) = Ordering.lt := compare_lt.mpr this
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝¹ : n < m
this✝ : k < j
this : n + k < m + j
⊢ compare (n + k) (m + j) = Ordering.lt
ℕ : Type
inst✝⁴ : Core ℕ
inst✝³ : Induction ℕ
inst✝² : Addition ℕ
inst✝¹ : Sign ℕ
order_inst : Order ℕ
inst✝ : Compare ℕ
ord : Ordering
n m k j : ℕ
x✝¹ : compare n m = Ordering.lt
x✝ : compare k j = Ordering.lt
this✝² : n < m
this✝¹ : k < j
this✝ : n + k < m + j
this : compare (n + k) (m + j) = Ordering.lt
⊢ compare (n + k) (m + j) = Ordering.lt