* Library/Order_Relation: new theory of various orderings as sets of pairs. Defines preorders, partial orders, linear orders and well-orders on sets and on types.