have : m + j < n + k := calc
  m + j < m + k := lt_substR_add ‹j < k›
  m + k < n + k := lt_substL_add ‹m < n›
ℕ : 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.gt
x✝ : compare k j = Ordering.gt
this✝ : n > m
this : k > j
⊢ compare (n + k) (m + j) = Ordering.gt
ℕ : 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.gt
x✝ : compare k j = Ordering.gt
this✝¹ : n > m
this✝ : k > j
this : m + j < n + k
⊢ compare (n + k) (m + j) = Ordering.gt