rw [bit_div_2, size_bit]
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size (bit b✝ n✝ / 2) = size (bit b✝ n✝) - 1
case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ size n✝ = succ (size n✝) - 1

case f
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : size (n✝ / 2) = size n✝ - 1
⊢ bit b✝ n✝ ≠ 0