Degree of univariate monomials

theorem Polynomial.natDegree_le_pred {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} (hf : p.natDegree ≤ n) (hn : p.coeff n = 0) : p.natDegree ≤ n - 1

theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : (Polynomial.monomial p.natDegree) p.leadingCoeff = p

theorem Polynomial.C_mul_X_pow_eq_self {R : Type u} [Semiring R] {p : Polynomial R} (h : p.support.card ≤ 1) : Polynomial.C p.leadingCoeff * Polynomial.X ^ p.natDegree = p