Theorem: getBit_zero_flipBit_succ (Controlbits/BitResiduum.lean)

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

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

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

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