induction' n using Nat.caseStrongInductionOn with n ih
n : ℕ
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑n ^ 3 - ↑n
case zero
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
⊢ 6 ∣ ↑0 ^ 3 - ↑0

case ind
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
n : ℕ
ih : ∀ m ≤ n, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ ↑(Nat.succ n) ^ 3 - ↑(Nat.succ n)