Theorem: condFlipBit_mul_cancel_right (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
ρ : Equiv.Perm (BV (a✝ + 1))
i : Fin (a✝ + 1)
c : BV a✝ → Bool
⊢ ρ * condFlipBit i c * condFlipBit i c = ρ
Tactic:
rw [mul_assoc, condFlipBit_mul_self, mul_one]
State after:
no goals