case z

⊢ List.length (bits 0) = size 0

case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (bits (bit b n)) = size (bit b n)
n : ℕ
⊢ List.length (bits n) = size n
induction' n using Nat.binaryRec' with b n h ih
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (b :: bits n) = succ (size n)

case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ bit b n ≠ 0
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (bits (bit b n)) = size (bit b n)
rw [size_bit, bits_append_bit _ _ h]
no goals
case z

⊢ List.length (bits 0) = size 0
simp
no goals
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ List.length (b :: bits n) = succ (size n)
simp [ih]
no goals
case f
b : Bool
n : ℕ
h : n = 0 → b = true
ih : List.length (bits n) = size n
⊢ bit b n ≠ 0
simpa [bit_eq_zero_iff]