R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.561231
hp : p ≠ 0
⊢ degree (erase (natDegree p) p) ≠ degree p
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.561231
hp : p ≠ 0
⊢ degree (erase (natDegree p) p) < degree p
apply lt_of_le_of_ne (degree_erase_le _ _)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.561231
hp : p ≠ 0
⊢ Finset.max (Finset.erase (support p) (natDegree p)) ≠ ↑(natDegree p)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.561231
hp : p ≠ 0
⊢ degree (erase (natDegree p) p) ≠ degree p
rw [degree_eq_natDegree hp, degree, support_erase]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.561231
hp : p ≠ 0
⊢ Finset.max (Finset.erase (support p) (natDegree p)) ≠ ↑(natDegree p)
exact fun h => not_mem_erase _ _ (mem_of_max h)