Theorem: flipBit_mul_cancel_left (Controlbits/BitResiduum.lean)

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