specialize hbx (le_trans ha hp)
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp✝ : Nat.Prime x
hp : 2 ≤ x
⊢ False
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hp✝ : Nat.Prime x
hp : 2 ≤ x
hbx : b ≤ x
⊢ False