R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ ↑n ≤ degree p

R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ p ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ n ≤ natDegree p
rw [← WithBot.coe_le_coe, ← Nat.cast_withBot,
  ← Nat.cast_withBot, ← degree_eq_natDegree]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ p ≠ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ ↑n ≤ degree p

R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ p ≠ 0
exact le_degree_of_ne_zero h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h✝ : coeff p n ≠ 0
h : p = 0
⊢ False
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ p ≠ 0
intro h
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
⊢ False
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h✝ : coeff p n ≠ 0
h : p = 0
⊢ False
subst h
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
⊢ False
exact h rfl