no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ natDegree p ≤ n ↔ ∀ (N : ℕ), n < N → coeff p N = 0
simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_withBot,
  WithBot.coe_lt_coe]