∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {s : Finset ι}
  {i : ι} {f g h : ι → R},
  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, 0 ≤ g i) → (∀ i ∈ s, 0 ≤ h i) → ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i