case hnc
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
s : σ
⊢ ¬0 = single s 1
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
s : σ
⊢ ↑(coeff R 0) (X s) = 0
rw [coeff_X, if_neg]
case hnc
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
s : σ
h : 0 = single s 1
⊢ False
case hnc
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
s : σ
⊢ ¬0 = single s 1
intro h
no goals
case hnc
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
s : σ
h : 0 = single s 1
⊢ False
exact one_ne_zero (single_eq_zero.mp h.symm)