∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] [MulLeftMono M]
  [MulRightStrictMono M] [MulRightMono M] {l : List ι},
  l ≠ [] → ∀ (f g : ι → M), (∀ i ∈ l, f i < g i) → (List.map f l).prod < (List.map g l).prod