∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial R) (n : ℕ),
  Polynomial.reflect n (Polynomial.map f p) = Polynomial.map f (Polynomial.reflect n p)