Theorem: flipBit_mul_cancel_right (Controlbits/BitResiduum.lean)

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