∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid A] [inst_4 : AddCommMonoid B] [AddLeftMono B] [AddRightMono B] {degb : A → B},
  degb 0 ≤ 0 →
    (∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
      ∀ (m : Multiset (AddMonoidAlgebra R A)),
        m.prod.support.sup degb ≤ (Multiset.map (fun f => f.support.sup degb) m).sum