Theorem: getBitRes_castSucc_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ (getBitRes i.castSucc) q =
    (((getBitRes i) ((getBitRes (Fin.last (m + 1))) q).2).1,
      (getBitRes (Fin.last m)).symm
        (((getBitRes (Fin.last (m + 1))) q).1, ((getBitRes i) ((getBitRes (Fin.last (m + 1))) q).2).2))
Tactic:
rw [getBitRes_castSucc, getBitResCastSucc_apply]
State after:
no goals