R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.703639
f : R[X]
n : ℕ
⊢ (∀ (m : ℕ), n ≤ m → coeff f m = 0) → degree f < ↑n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.703639
f : R[X]
n : ℕ
⊢ degree f < ↑n ↔ ∀ (m : ℕ), n ≤ m → coeff f m = 0
refine'
  ⟨fun hf m hm => coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hf (WithBot.coe_le_coe.2 hm)), _⟩
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.703639
f : R[X]
n : ℕ
⊢ (∀ (m : ℕ), n ≤ m → coeff f m = 0) → ∀ (b : ℕ), coeff f b ≠ 0 → ¬n ≤ b
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.703639
f : R[X]
n : ℕ
⊢ (∀ (m : ℕ), n ≤ m → coeff f m = 0) → degree f < ↑n
simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff, WithBot.some_eq_coe,
  WithBot.coe_lt_coe, ← @not_le ℕ, max_eq_sup_coe, Nat.cast_withBot]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.703639
f : R[X]
n : ℕ
⊢ (∀ (m : ℕ), n ≤ m → coeff f m = 0) → ∀ (b : ℕ), coeff f b ≠ 0 → ¬n ≤ b
exact fun h m => mt (h m)