Theorem: flipBit_ne_self (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ (flipBit i) q ≠ q
Tactic:
apply ne_of_getBit_ne i
State after:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ getBit i ((flipBit i) q) ≠ getBit i q

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ getBit i ((flipBit i) q) ≠ getBit i q
Tactic:
rw [getBit_flipBit, ne_eq, Bool.not_not_eq]
State after:
no goals