Require Export Relation_Definitions.

Arguments reflexive {A}.
Arguments transitive {A}.
Arguments symmetric {A}.
Arguments antisymmetric {A}.
Arguments equiv {A}.
Arguments preorder {A}.
Arguments Build_preorder {A}.
Arguments preord_refl {A} {R}.
Arguments preord_trans {A} {R}.
Arguments order {A}.
Arguments Build_order {A}.
Arguments ord_refl {A} {R}.
Arguments ord_trans {A} {R}.
Arguments ord_antisym {A} {R}.
Arguments equivalence {A}.
Arguments Build_equivalence {A}.
Arguments equiv_refl {A} {R}.
Arguments equiv_trans {A} {R}.
Arguments equiv_sym {A} {R}.
Arguments PER {A}.
Arguments Build_PER {A}.
Arguments per_sym {A} {R}.
Arguments per_trans {A} {R}.
Arguments inclusion {A}.
Arguments same_relation {A}.
Arguments commut {A}.
