case h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
⊢ degree p < ↑n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
⊢ coeff p n = 0
apply coeff_eq_zero_of_degree_lt
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
hp : p = 0
⊢ degree p < ↑n

case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
hp : ¬p = 0
⊢ degree p < ↑n
case h
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
⊢ degree p < ↑n
by_cases hp : p = 0
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
hp : p = 0
⊢ degree p < ↑n
subst hp
no goals
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n
exact WithBot.bot_lt_coe n
no goals
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : natDegree p < n
hp : ¬p = 0
⊢ degree p < ↑n
rwa [degree_eq_natDegree hp, Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe]