This file contains the basic API for "pushing through" the isomorphism
opRingEquiv : R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]. It allows going back and forth between a polynomial ring
over a semiring and the polynomial ring over the opposite semiring.
Lemmas about more global properties of polynomials and opposites.