simp only [sumDrop, powers, pow_succ, pow_zero, mul_one, 
  dropEveryNth_eq_fun, pnats, Nat.div_one
]
case h
i : ℕ
⊢ sumDrop 4 pnats i = powers 4 i
case h
i : ℕ
⊢ sum (fun i => sum (fun i => sum (fun i => i + i / 3 + 1) (i + i / 2)) (i + i)) i =
    (i + 1) * ((i + 1) * ((i + 1) * (i + 1)))