m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
m : ℕ
b : Bool
n : ℕ
⊢ testBit (bit b n) (succ m) = testBit n m
have : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m) := by
  dsimp [shiftr]
  rw [div2_bit]
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (bit b n) (m + 1)) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
rw [← shiftr_add, Nat.add_comm] at this
no goals
m : ℕ
b : Bool
n : ℕ
this : bodd (shiftr (bit b n) (m + 1)) = bodd (shiftr n m)
⊢ testBit (bit b n) (succ m) = testBit n m
exact this
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (div2 (bit b n)) m) = bodd (shiftr n m)
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m)
dsimp [shiftr]
no goals
m : ℕ
b : Bool
n : ℕ
⊢ bodd (shiftr (div2 (bit b n)) m) = bodd (shiftr n m)
rw [div2_bit]