have : (24 : ℤ) = 6 * 4 := by ring
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
⊢ 6 ∣ 24
case pos.step.refl
gt_pow3 : ∀ (n : ℕ), n ≤ n ^ 3
ih : ∀ m ≤ 2, 6 ∣ ↑m ^ 3 - ↑m
this : 24 = 6 * 4
⊢ 6 ∣ 24