case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
⊢ degree p < degree q

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : ¬p = 0
⊢ degree p < degree q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
⊢ degree p < degree q
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[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
⊢ ⊥ < degree q
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
⊢ degree p < degree q
simp [hp]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
⊢ degree q ≠ ⊥
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
⊢ ⊥ < degree q
rw [bot_lt_iff_ne_bot]
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
hq : degree q = ⊥
⊢ False
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
⊢ degree q ≠ ⊥
intro hq
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : p = 0
hq : degree q = ⊥
⊢ False
simp [hp, degree_eq_bot.mp hq, lt_irrefl] at h
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : ¬p = 0
⊢ ↑(natDegree p) < ↑(natDegree q)
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : ¬p = 0
⊢ degree p < degree q
rw [degree_eq_natDegree hp, degree_eq_natDegree <| ne_zero_of_natDegree_gt h,
  Nat.cast_withBot, Nat.cast_withBot]
no goals
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.467624
h : natDegree p < natDegree q
hp : ¬p = 0
⊢ ↑(natDegree p) < ↑(natDegree q)
exact_mod_cast h