Theorem: condFlipBit_comm_flipBit (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
⊢ condFlipBit i c * flipBit i = flipBit i * condFlipBit i c
Tactic:
rw [condFlipBit_flipBit_of_all_true, condFlipBit_comm]
State after:
no goals