∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α) (f : α → β)
  (comm : (↑(insert a s)).Pairwise (Function.onFun AddCommute f)),
  a ∉ s → (insert a s).noncommSum f comm = s.noncommSum f ⋯ + f a