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

case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ natDegree (p * mirror p) = 2 * natDegree p
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ natDegree (p * mirror p) = 2 * natDegree 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
⊢ natDegree (p * mirror p) = 2 * natDegree p
rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]
no goals
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natDegree (p * mirror p) = 2 * natDegree p
rw [hp, MulZeroClass.zero_mul, natDegree_zero, MulZeroClass.mul_zero]