repeat rw [← Nat.Ico_succ_succ]
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n) ⊆ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ∪ Finset.Ioc (2 * n / 3) (2 * n)
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)) ⊆
    Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n / 3)) ∪
      Finset.Ico (Nat.succ (2 * n / 3)) (Nat.succ (2 * n))