case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p

case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : ¬p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
by_cases hp : p = 0
no goals
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : ¬p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
rw [trailingDegree_eq_natTrailingDegree hp]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree 0) ≤ ⊤
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree p) ≤ 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 : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree 0) ≤ ⊤
exact le_top