Some lemmas about the deglex monomial order on multivariate polynomials

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

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