Products of star-ordered rings

instance Prod.instStarOrderedRing {α : Type u_1} {β : Type u_2} [NonUnitalSemiring α] [NonUnitalSemiring β] [PartialOrder α] [PartialOrder β] [StarRing α] [StarRing β] [StarOrderedRing α] [StarOrderedRing β] : StarOrderedRing (α × β)