(cl-module Partial_Order_From_Strict_Partial_Order
  (cl-imports Strict_Partial_Order.clif)
  (cl-comment 'reflexive')
  (forall (x)
          (le x x))
  (cl-comment 'antisymmetric')
  (forall (x y)
          (if (and (le x y)
                   (le y x))
              (= x y)))
  (cl-comment 'transitive')
  (forall (x y z)
          (if (and (le x y)
                   (le y z))
              (le x z))))