unfold ones
b m n : ℕ
⊢ ones b (m + n) = ones b m + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
b m n : ℕ
⊢ (let k := m + n;
    Nat.ofDigits b (List.replicate k 1)) =
    (let k := m;
      Nat.ofDigits b (List.replicate k 1)) +
      Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)