no goals
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ leadingCoeff (reverse f) = trailingCoeff f
rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
  coeff_reverse, revAt_invol, trailingCoeff]