Theorem: condFlipBit_zero_apply (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit 0 c) q = bif c q.divNat then finProdFinEquiv (q.divNat, q.modNat.rev) else q
Tactic:
rw [condFlipBit_apply, flipBit_zero_apply, getRes_zero]
State after:
no goals