cases' lt_or_le 511 n with h h
n : ℕ
hn0 : n ≠ 0
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n