Some lemmas about the deglex monomial order on multivariate polynomials

theorem MvPolynomial.degree_degLexDegree {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} [LinearOrder σ] [WellFoundedGT σ] : (MonomialOrder.degLex.degree f).degree = 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

theorem MvPolynomial.totalDegree_mul_of_isDomain {σ : Type u_1} {R : Type u_2} [CommSemiring R] {f g : MvPolynomial σ R} [IsCancelMulZero R] (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).totalDegree = f.totalDegree + g.totalDegree