∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {ι : Type u_2}
  [inst_3 : LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M},
  StrictMonoOn (ArchimedeanClass.mk ∘ a) ↑s →
    ArchimedeanClass.mk (∑ i ∈ s, a i) = ArchimedeanClass.mk (a (s.min' hnonempty))