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