Monotone Finsupp.prod

Stream: Is there code for X?

[Snir Broshi]

f₁ ≤ f₂ → f₁.prod g ≤ f₂.prod g and f₁ < f₂ → f₁.prod g < f₂.prod g aren't always true, but I think they're true given some trivial restrictions:

import Mathlib

theorem Finsupp.prod_monotone {α M N : Type*} [Zero M] [Preorder M] [CommMonoid N] [Preorder N]
    {f₁ f₂ : α →₀ M} {g : α → M → N} (h : ∀ a ∈ f₂.support, MonotoneOn (g a) {0}ᶜ)
    (h' : ∀ a ∈ f₂.support, ∀ x, x ≤ x * (g a (f₂ a))) : f₁ ≤ f₂ → f₁.prod g ≤ f₂.prod g := by
  sorry

theorem Finsupp.prod_strictMono {α M N : Type*} [Zero M] [Preorder M] [Zero N] [CommMonoid N]
    [Preorder N] {f₁ f₂ : α →₀ M} {g : α → M → N} (h : ∀ a ∈ f₂.support, StrictMonoOn (g a) {0}ᶜ)
    (h' : ∀ a ∈ f₂.support, ∀ x ∈ ({0}ᶜ : Set N), x < x * (g a (f₂ a))) :
    f₁ < f₂ → f₁.prod g < f₂.prod g := by
  sorry

Does this exist in some form?
Also, are there parts in the statement that have existing defs? e.g. ∀ x, x ≤ x * c reminds me of IsRightRegular c

[Snir Broshi]

The motivation is from the case where f₁ and f₂ have only primes in their support, and g = (· ^ ·), so this is a statement relating prime factorizations