include "basics/types.ma".

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