∀ {w hi lo i : ℕ},
  i < hi - lo + 1 →
    max hi lo - i < w →
      w - 1 - (lo + (hi - lo + 1 - 1 - i)) = w - 1 - (max hi lo - i) →
        ¬(i < hi - lo + 1 ∧ hi - lo - i < hi - lo + 1 ∧ lo + (hi - lo - i) < w) → False