no goals
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
n : ℕ
H1 : degree p ≤ ↑n
H2 : coeff p n = 1
H : ¬degree p < ↑n
⊢ Monic p
rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]