Theorem: getRes_apply_two_pow (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ getRes i ⟨2 ^ ↑i, ⋯⟩ = 0
Tactic:
rw [getRes_apply, getBitRes_apply_two_pow]
State after:
no goals