Theorem: sumDrop_two (ListPowersProblem.lean)

State before:
⊢ sumDrop 2 pnats = powers 2
Tactic:
simp only [sumDrop]
State after:
⊢ sum (dropEveryNth (1 + 1) pnats) = powers 2

State before:
⊢ sum (dropEveryNth (1 + 1) pnats) = powers 2
Tactic:
rw [procedure_two_eq_squares]
State after:
no goals