∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] {ι : Type u_2} (f g : ι → R) (a : ι)
  (s : List ι),
  ((∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → (List.map f s).prod ≤ (List.map g s).prod) →
    (∀ i ∈ a :: s, 0 ≤ f i) → (∀ i ∈ a :: s, f i ≤ g i) → (List.map f s).prod ≤ (List.map g s).prod