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

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natDegree (mirror p) = natDegree p
R : Type u_1
inst✝ : Semiring R
p q : R[X]
⊢ natDegree (mirror p) = natDegree p
by_cases hp : p = 0
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ natDegree (mirror p) = natDegree p
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
⊢ natDegree (mirror p) = natDegree p
nontriviality R
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ leadingCoeff (reverse p) * leadingCoeff (X ^ natTrailingDegree p) ≠ 0
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ natDegree (mirror p) = natDegree p
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
  tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
no goals
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : ¬p = 0
✝ : Nontrivial R
⊢ leadingCoeff (reverse p) * leadingCoeff (X ^ natTrailingDegree p) ≠ 0
rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]
no goals
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
hp : p = 0
⊢ natDegree (mirror p) = natDegree p
rw [hp, mirror_zero]