プレ順序集合とその実例

structure PreOrder where
 U : Type
 le : U → U → Prop
 le_refl : ∀(x : U), le x x
 le_trans : ∀(x y z: U), (le x y ∧ le y z) → le x z

inductive ab where 
  | a
  | b

def ab_le (x : ab) (y : ab) : Prop :=
  match (x, y) with
  | (.a, _) => True
  | (.b, .a) => False
  | (.b, .b) => True

{U := ab, le := ab_le, .. } が実例になるには、le_refl, le_trans の証明が必要。