R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree 0 = ↑n
hp0 : p = 0
⊢ False
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree p = ↑n
hp0 : p = 0
⊢ False
rw [hp0] at h
no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree 0 = ↑n
hp0 : p = 0
⊢ False
exact Option.noConfusion h
no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree p = ↑n
hp0 : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n
rwa [← trailingDegree_eq_natTrailingDegree hp0]