case z
n : ℕ
⊢ bodd 0 = List.headI (bits 0)

case f
n✝ : ℕ
b : Bool
n : ℕ
h : n = 0 → b = true
a✝ : bodd n = List.headI (bits n)
⊢ bodd (bit b n) = List.headI (bits (bit b n))
n✝ n : ℕ
⊢ bodd n = List.headI (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✝ : bodd n = List.headI (bits n)
⊢ bodd (bit b n) = List.headI (bits (bit b n))
simp [bodd_bit, bits_append_bit _ _ h]
no goals
case z
n : ℕ
⊢ bodd 0 = List.headI (bits 0)
simp