∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : PartialOrder α] [MulLeftStrictMono α]
  [inst_3 : CommMonoid β] [inst_4 : PartialOrder β] [IsOrderedMonoid β], IsOrderedMonoid (Lex (α × β))