no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.701471
⊢ natDegree p = 0 ↔ degree p ≤ 0
rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le,
  Nat.cast_withBot, WithBot.coe_zero]