. simp [hp]
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0

case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1