∀ {ι : Type u_1} {R : Type u_2} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R]
  (s : Finset ι) (f : ι → R) {g : ι → R},
  (∀ i ∈ s, 0 < g i) → (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i