no goals
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]),
    natDegree (Multiset.sum (Quotient.mk (List.isSetoid S[X]) a)) ≤
      foldr max (_ : ∀ (a b c : ℕ), max a (max b c) = max b (max a c)) 0
        (Multiset.map natDegree (Quotient.mk (List.isSetoid S[X]) a))
simpa using natDegree_list_sum_le