case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < degree p ↔ n < natDegree p

case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < degree p ↔ n < natDegree p
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
⊢ ↑n < degree p ↔ n < natDegree p
by_cases h : p = 0
no goals
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : ¬p = 0
⊢ ↑n < degree p ↔ n < natDegree p
simp [degree_eq_natDegree h, Nat.cast_withBot, WithBot.coe_lt_coe]
no goals
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < degree p ↔ n < natDegree p
simp [h]