Theorem: flipBit_castSucc (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
q : BV (a✝ + 1 + 1)
i : Fin (a✝ + 1)
⊢ (flipBit i.castSucc) q =
    mergeBitRes (Fin.last (a✝ + 1)) (getBit (Fin.last (a✝ + 1)) q) ((flipBit i) (getRes (Fin.last (a✝ + 1)) q))
Tactic:
simp_rw [flipBit_apply, getBit_castSucc, getRes_castSucc, mergeBitRes_castSucc,
getBit_mergeBitRes, getRes_mergeBitRes]
State after:
no goals