case h
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ ↑n < trailingDegree p
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ coeff p n = 0
apply coeff_eq_zero_of_trailingDegree_lt
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < trailingDegree p

case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < trailingDegree p
case h
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ ↑n < trailingDegree p
by_cases hp : p = 0
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < ⊤
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < trailingDegree p
rw [hp, trailingDegree_zero]
no goals
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < ⊤
exact WithTop.coe_lt_top n
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < ↑(natTrailingDegree p)
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < trailingDegree p
rw [trailingDegree_eq_natTrailingDegree hp]
no goals
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < ↑(natTrailingDegree p)
exact WithTop.coe_lt_coe.2 h