∀ {k : Type u_1} [inst : Ring k] [inst_1 : PartialOrder k] {n : ℕ} {fs : Finset (Fin (n + 1))} {w : Fin (n + 1) → k},
  ((∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0) → (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0