∀ {l l' r : ℕ},
  l + r ≤ 1 ∨ l ≤ 3 * r ∧ r ≤ 3 * l →
    l - 1 ≤ l' →
      l' ≤ l + 1 →
        ¬((3 * l' ≤ 3 * 3 * r + 3 * r + r + 3 ∧ r + 1 ≤ l' ∨
                (l' + (r + 1) ≤ 1 ∨ l' ≤ 3 * (r + 1) ∧ r + 1 ≤ 3 * l') ∨ l' + r ≤ 1 ∨ l' ≤ 3 * r ∧ r ≤ 3 * l') ∨
              3 * r ≤ 3 * 3 * l' + 3 * l' + l' + 3 ∧ l' + 1 ≤ r ∨
                (r + (l' + 1) ≤ 1 ∨ r ≤ 3 * (l' + 1) ∧ l' + 1 ≤ 3 * r) ∨ r + l' ≤ 1 ∨ r ≤ 3 * l' ∧ l' ≤ 3 * r) →
          False