Products of ordered rings

instance instIsOrderedRingProd {α : Type u_1} {β : Type u_2} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Semiring β] [PartialOrder β] [IsOrderedRing β] : IsOrderedRing (α × β)