Theorem: Nat.bit_div_2 (Lib.lean)

State before:
b : Bool
n : ℕ
⊢ bit b n / 2 = n
Tactic:
set_option linter.deprecated false in
cases b <;> dsimp [bit, bit0, bit1] <;> omega
State after:
no goals

State before:
b : Bool
n : ℕ
⊢ bit b n / 2 = n
Tactic:
cases b <;> dsimp [bit, bit0, bit1] <;> omega
State after:
no goals