Theorem: ne_iff_getBit_ne_or_getRes_ne (Controlbits/BitResiduum.lean)

State before:
m : ℕ
q₁ q₂ : BV (m + 1)
i : Fin (m + 1)
⊢ q₁ ≠ q₂ ↔ getBit i q₁ ≠ getBit i q₂ ∨ getRes i q₁ ≠ getRes i q₂
Tactic:
rw [ne_eq q₁, getRes_getBit_inj_iff i, not_and_or]
State after:
no goals