include "basics/types.ma".

inductive order: Type[0] ≝
  | order_lt: order
  | order_gt: order
  | order_eq: order.

record ordered (elt_type: Type[0]): Type[1] ≝
{
  order: elt_type → elt_type → order
}.