case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
by_cases hp : p = 0
no goals
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
rw [hp, mirror_zero]
no goals
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natTrailingDegree (mirror p) = natTrailingDegree p
rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
  reverse_natTrailingDegree, zero_add]