Theorem: flipBit_succ (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
q : BV (a✝ + 1 + 1)
i : Fin (a✝ + 1)
⊢ (flipBit i.succ) q = mergeBitRes 0 (getBit 0 q) ((flipBit i) (getRes 0 q))
Tactic:
simp_rw [flipBit_apply, getBit_succ, getRes_succ, mergeBitRes_succ,
getBit_mergeBitRes, getRes_mergeBitRes]
State after:
no goals