no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.702057
f : R[X]
n : WithBot ℕ
⊢ degree f ≤ n ↔ ∀ (m : ℕ), n < ↑m → coeff f m = 0
simp only [degree, Finset.max, Finset.sup_le_iff, mem_support_iff, Ne.def, ← not_le,
  not_imp_comm, Nat.cast_withBot]