case z
n : ℕ
⊢ bits (div2 0) = List.tail (bits 0)

case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bits (div2 n) = List.tail (bits n)
⊢ bits (div2 (bit b n)) = List.tail (bits (bit b n))
n✝ n : ℕ
⊢ bits (div2 n) = List.tail (bits n)
induction' n using Nat.binaryRec' with b n h _
no goals
case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bits (div2 n) = List.tail (bits n)
⊢ bits (div2 (bit b n)) = List.tail (bits (bit b n))
simp [div2_bit, bits_append_bit _ _ h]
no goals
case z
n : ℕ
⊢ bits (div2 0) = List.tail (bits 0)
simp