Some lemmas about the degree lexicographic monomial order on multivariate polynomials

theorem MvPolynomial.degree_degLexDegree {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} [LinearOrder σ] [WellFoundedGT σ] : Finsupp.degree (MonomialOrder.degLex.degree f) = f.totalDegree

theorem MvPolynomial.degLex_totalDegree_monotone {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} [LinearOrder σ] [WellFoundedGT σ] (h : MonomialOrder.degLex.toSyn (MonomialOrder.degLex.degree f) ≤ MonomialOrder.degLex.toSyn (MonomialOrder.degLex.degree g)) : f.totalDegree ≤ g.totalDegree