rcases hp with _ | hp
case pos.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 2
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(2 + 1) ^ 3 - ↑(2 + 1)

case pos.step.step
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : Nat.le n 1
⊢ 6 ∣ ↑(n + 1) ^ 3 - ↑(n + 1)