∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R]
  {f g h : ι → R} {s : Finset ι} {i : ι},
  i ∈ s →
    g i + h i ≤ f i →
      (∀ j ∈ s, j ≠ i → g j ≤ f j) → (∀ j ∈ s, j ≠ i → h j ≤ f j) → ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i