have h6 : n - m < N := by
  calc
    _ < n := sub_lt_self n h1.m_range.left
    _ ≤ N := h1.n_range.right
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
⊢ n - m ∈ Ioc 0 ↑N
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
h5 : 0 < n - m
h6 : n - m < ↑N
⊢ n - m ∈ Ioc 0 ↑N