∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R]
  [PosMulStrictMono R] [Nontrivial R] {f g : ι → R} {s : Finset ι},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → ∏ i ∈ s, f i < ∏ i ∈ s, g i