R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p ≤ n
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ natTrailingDegree p ≤ n
have : WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := rfl
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p ≤ ↑n

R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ p ≠ 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p ≤ n
rw [← WithTop.coe_le_coe, this, ← trailingDegree_eq_natTrailingDegree]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p ≤ ↑n
exact le_trailingDegree_of_ne_zero h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h✝ : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
h : p = 0
⊢ False
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ p ≠ 0
intro h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
this : ↑(natTrailingDegree 0) = ↑(natTrailingDegree 0)
⊢ False
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h✝ : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
h : p = 0
⊢ False
subst h
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
this : ↑(natTrailingDegree 0) = ↑(natTrailingDegree 0)
⊢ False
exact h rfl