exact
  { n_range := h1.m_range
    m_range := by
      have h5 : 0 < n - m := sub_pos.mpr h3
      have h6 : n - m < N := by
        calc
          _ < n := sub_lt_self n h1.m_range.left
          _ ≤ N := h1.n_range.right
      exact ⟨h5, h6.le⟩
    eq_one := by linear_combination h1.eq_one }
case inr
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ ProblemPredicate N (n - m) m
no goals