∀ {R : Type u_1} {σ : Type u_2} {n : σ} [inst : CommSemiring R] {p q : MvPolynomial σ R} [NoZeroDivisors R],
  p ≠ 0 → q ≠ 0 → MvPolynomial.degreeOf n (p * q) = MvPolynomial.degreeOf n p + MvPolynomial.degreeOf n q