Theorem: mergeBitRes_ne_iff (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
q : BV (a✝ + 1)
⊢ mergeBitRes i b p ≠ q ↔ getBit i q ≠ b ∨ getRes i q ≠ p
Tactic:
simp_rw [ne_eq, mergeBitRes_eq_iff, Decidable.not_and_iff_or_not]
State after:
no goals