case hnc
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natDegree p
⊢ ¬natDegree p = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natDegree p
⊢ nextCoeff p = coeff p (natDegree p - 1)
rw [nextCoeff, if_neg]
case hnc
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p = 0
⊢ natDegree p ≤ 0
case hnc
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natDegree p
⊢ ¬natDegree p = 0
contrapose! hp
no goals
case hnc
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : natDegree p = 0
⊢ natDegree p ≤ 0
simpa