Theorem: getRes_castSucc (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ getRes i.castSucc q = mergeBitRes (Fin.last m) (getBit (Fin.last (m + 1)) q) (getRes i (getRes (Fin.last (m + 1)) q))
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, getBit_apply, getBitRes_castSucc_apply]
State after:
no goals