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
  }.