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