no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ trailingCoeff (mirror p) = leadingCoeff p
rw [leadingCoeff, trailingCoeff, mirror_natTrailingDegree, coeff_mirror,
  revAt_le (Nat.le_add_left _ _), add_tsub_cancel_right]