induction n using Nat.binaryRec' with
| z => exact le_refl _
| f b n hb ih =>
  rw [size_bit]
  cases b
  simp
  apply Nat.add_le_add (c := 1) ih
  { cases n
    exact absurd (hb rfl) Bool.noConfusion
    exact Nat.succ_le_succ (Nat.zero_le _) }
  simp
  apply Nat.succ_le_succ
  apply le_trans
  apply ih
  apply le_add_left
  cases b
  simpa using λ h ↦ absurd (hb h) Bool.noConfusion
  simp
n : ℕ
⊢ size n ≤ n
no goals