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