by_cases h : p ≤ 2 * n
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
case pos
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case neg
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n