R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ coeff f (↑(revAt (natDegree f)) 1) = if natDegree f = 0 then 0 else coeff f (natDegree f - 1)
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ coeff (reverse f) 1 = nextCoeff f
rw [coeff_reverse, nextCoeff]
case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = 0

case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬natDegree f = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = coeff f (natDegree f - 1)
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ coeff f (↑(revAt (natDegree f)) 1) = if natDegree f = 0 then 0 else coeff f (natDegree f - 1)
split_ifs with hf
case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
this : coeff f 1 = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = 0
case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = 0
have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])
no goals
case inl
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
this : coeff f 1 = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = 0
simp [*, revAt]
no goals
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
⊢ natDegree f < 1
simp only [hf, zero_lt_one]
case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬natDegree f = 0
⊢ 1 ≤ natDegree f
case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬natDegree f = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = coeff f (natDegree f - 1)
rw [revAt_le]
no goals
case inr
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬natDegree f = 0
⊢ 1 ≤ natDegree f
exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)