case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
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 : R[X]
h : coeff q (natDegree p) ≠ 0
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 : R[X]
h : coeff q (natDegree p) ≠ 0
⊢ 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 : R[X]
h : coeff q (natDegree p) ≠ 0
hp : p = 0
⊢ degree 0 ≤ degree q
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : p = 0
⊢ degree p ≤ degree q
rw [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]
h : coeff q (natDegree p) ≠ 0
hp : p = 0
⊢ degree 0 ≤ degree q
exact bot_le
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : ¬p = 0
⊢ ↑(natDegree p) ≤ degree q
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : ¬p = 0
⊢ degree p ≤ degree q
rw [degree_eq_natDegree hp]
no goals
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natDegree p) ≠ 0
hp : ¬p = 0
⊢ ↑(natDegree p) ≤ degree q
exact le_degree_of_ne_zero h