cases n using Nat.binaryRec' with
| z => exact z
| f b n hb =>
  cases b with
  | true => simpa [← Nat.two_mul] using o _
  | false =>
    match n with
    | 0 => exact absurd (hb rfl) Bool.noConfusion
    | n+1 => simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n : ℕ
⊢ C n
no goals