no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.736582
hdeg : ↑n ≤ degree p
⊢ ↑n ≤ ↑(natDegree p)
rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg