Theorem: getBit_succAbove (Controlbits/BitResiduum.lean)

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