Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
⊢ r = (flipBit 0) q
Tactic:
rcases getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt h hf with ⟨hr, hq, hrq⟩
State after:
case intro.intro
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
hr : getBit 0 r = false
hq : getBit 0 q = true
hrq : getRes 0 r = getRes 0 q
⊢ r = (flipBit 0) q

State before:
case intro.intro
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
hr : getBit 0 r = false
hq : getBit 0 q = true
hrq : getRes 0 r = getRes 0 q
⊢ r = (flipBit 0) q
Tactic:
simp only [eq_flipBit_iff, hr, hq, hrq, Bool.not_true, and_self]
State after:
no goals