∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {ι : Type u_7} {s : Finset ι} {f : ι → R} {g : Γ₀}, g ≠ 0 → (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g