Theorem: flipBit_succAbove (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
q : BV (m + 1 + 1)
j : Fin (m + 2)
⊢ (flipBit (j.succAbove i)) q = mergeBitRes j (getBit j q) ((flipBit i) (getRes j q))
Tactic:
simp_rw [flipBit_apply, getBit_succAbove, getRes_succAbove, mergeBitRes_succAbove,
getBit_mergeBitRes, getRes_mergeBitRes]
State after:
no goals