Library CT.Order.PartiallyOrderedSet

Record PartiallyOrderedSet {element : Type} :=
  { le : element element Prop;
    reflexive : a, le a a;
    transitive : a b c, le a b le b c le a c;
    antisymmetric : a b, le a b le b a a = b
  }.