Degree of univariate monomials

theorem Polynomial.natDegree_le_pred {R : Type u} {n : Nat} [Semiring R] {p : Polynomial R} (hf : LE.le p.natDegree n) (hn : Eq (p.coeff n) 0) : LE.le p.natDegree (HSub.hSub n 1)

theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : LE.le p.support.card 1) : Eq (DFunLike.coe (monomial p.natDegree) p.leadingCoeff) p

theorem Polynomial.C_mul_X_pow_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : LE.le p.support.card 1) : Eq (HMul.hMul (DFunLike.coe C p.leadingCoeff) (HPow.hPow X p.natDegree)) p