∀ {α : Type u_1} [inst : AddMonoid α] (n : ℕ) (a : WithTop α),
  (match a, n + 1 with
    | some a, n => ↑(n • a)
    | none, 0 => 0
    | none, _n.succ => ⊤) =
    (match a, n with
      | some a, n => ↑(n • a)
      | none, 0 => 0
      | none, _n.succ => ⊤) +
      a