∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R] [inst_2 : Add R] (x : ℕ),
  x.binCast =
    match x with
    | 0 => 0
    | n.succ =>
      if (n + 1) % 2 = 0 then ((n + 1) / 2).binCast + ((n + 1) / 2).binCast
      else ((n + 1) / 2).binCast + ((n + 1) / 2).binCast + 1