R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
fg : leadingCoeff f * leadingCoeff g ≠ 0
⊢ reflect (natDegree (f * g)) (f * g) = reflect (natDegree f) f * reflect (natDegree g) g
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
fg : leadingCoeff f * leadingCoeff g ≠ 0
⊢ reverse (f * g) = reverse f * reverse g
unfold reverse
no goals
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
fg : leadingCoeff f * leadingCoeff g ≠ 0
⊢ reflect (natDegree (f * g)) (f * g) = reflect (natDegree f) f * reflect (natDegree g) g
rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]