Theorem: ne_mergeBitRes_iff (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
q : BV (a✝ + 1)
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ q ≠ mergeBitRes i b p ↔ getBit i q ≠ b ∨ getRes i q ≠ p
Tactic:
rw [← mergeBitRes_ne_iff, ne_comm]
State after:
no goals