R : Type u
S : Type ?u.48578
inst✝ : Semiring R
p : R[X]
n : ℕ
h : coeff p n ≠ 0
⊢ ∃ a, ¬coeff p a = 0 ∧ coeff p a = coeff p n
R : Type u
S : Type ?u.48578
inst✝ : Semiring R
p : R[X]
n : ℕ
h : coeff p n ≠ 0
⊢ coeff p n ∈ frange p
simp only [frange, exists_prop, mem_support_iff, Finset.mem_image, Ne.def]
no goals
R : Type u
S : Type ?u.48578
inst✝ : Semiring R
p : R[X]
n : ℕ
h : coeff p n ≠ 0
⊢ ∃ a, ¬coeff p a = 0 ∧ coeff p a = coeff p n
exact ⟨n, h, rfl⟩