Theorem: getBit_succ_flipBit_zero (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q : BV (m + 1)
i : Fin m
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Tactic:
cases m
State after:
case zero
q : BV (0 + 1)
i : Fin 0
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q

case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i : Fin (n✝ + 1)
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q

State before:
case zero
q : BV (0 + 1)
i : Fin 0
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Tactic:
exact i.elim0
State after:
no goals

State before:
case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i : Fin (n✝ + 1)
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Tactic:
simp_rw [getBit_succ, getRes_flipBit]
State after:
no goals