case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
p0 : natDegree p = 0
⊢ natDegree (↑derivative p) ≤ natDegree p - 1

case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
p0 : ¬natDegree p = 0
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
by_cases p0 : p.natDegree = 0
no goals
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
p0 : natDegree p = 0
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
simp [p0, derivative_of_natDegree_zero]
no goals
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p : R[X]
p0 : ¬natDegree p = 0
⊢ natDegree (↑derivative p) ≤ natDegree p - 1
exact Nat.le_pred_of_lt (natDegree_derivative_lt p0)