rw [hk]
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)
case neg
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
hp : ¬n ≤ 3
k : ℕ := n - 3
hk : Nat.succ n = k + 4
⊢ 6 ∣ ↑(k + 4) ^ 3 - ↑(k + 4)