Theorem: mergeBitRes_succAbove (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b : Bool
q : BV (m + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ mergeBitRes (j.succAbove i) b q =
    mergeBitRes j (getBit (i.predAbove j) q) (mergeBitRes i b (getRes (i.predAbove j) q))
Tactic:
simp_rw [mergeBitRes_apply, getBit_apply, getRes_apply, getBitRes_succAbove_symm_apply]
State after:
no goals