∀ {R : Type u_1} [inst : Semiring R] (r : Rᵐᵒᵖ) (n : ℕ),
  (Polynomial.opRingEquiv R).symm (Polynomial.C r * Polynomial.X ^ n) =
    MulOpposite.op (Polynomial.C (MulOpposite.unop r) * Polynomial.X ^ n)