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

case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
by_cases hp : p = 0
no goals
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]
no goals
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natTrailingDegree (p * mirror p) = 2 * natTrailingDegree p
rw [hp, MulZeroClass.zero_mul, natTrailingDegree_zero, MulZeroClass.mul_zero]