case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a

case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : ¬a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
by_cases ha : a = 0
no goals
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
rw [ha, monomial_zero_right, mirror_zero]
no goals
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
ha : ¬a = 0
⊢ mirror (↑(monomial n) a) = ↑(monomial n) a
rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
  C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
  mul_one]