-include "higher_order_defs/relations.ma".
-include "nat/plus.ma".
-include "constructive_connectives.ma".
-
-definition cotransitive ≝
- λC:Type.λle:C→C→Prop.∀x,y,z:C. le x y → le x z ∨ le z y.
-
-definition antisimmetric ≝
- λC:Type.λle:C→C→Prop.∀x,y:C. le x y → le y x → x=y.
-
-record is_order_relation (C:Type) (le:C→C→Prop) : Type ≝
- { or_reflexive: reflexive ? le;
- or_transitive: transitive ? le;
- or_antisimmetric: antisimmetric ? le
- }.
-
-record ordered_set: Type ≝
- { os_carrier:> Type;
- os_le: os_carrier → os_carrier → Prop;
- os_order_relation_properties:> is_order_relation ? os_le
- }.
-
-interpretation "Ordered Sets le" 'leq a b =
- (cic:/matita/ordered_sets/os_le.con _ a b).
-
+include "excedence.ma".
+
+record is_porder_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ {
+ por_reflexive: reflexive ? le;
+ por_transitive: transitive ? le;
+ por_antisimmetric: antisymmetric ? le eq
+}.
+
+record pordered_set: Type ≝ {
+ pos_carr:> excedence;
+ pos_order_relation_properties:> is_porder_relation ? (le pos_carr) (eq pos_carr)
+}.
+
+lemma pordered_set_of_excedence: excedence → pordered_set.
+intros (E); apply (mk_pordered_set E); apply (mk_is_porder_relation);
+[apply le_reflexive|apply le_transitive|apply le_antisymmetric]
+qed.
+
+definition total_order : ∀E:excedence. Type ≝
+ λE:excedence. ∀a,b:E. a ≰ b → a < b.
+
+alias id "transitive" = "cic:/matita/higher_order_defs/relations/transitive.con".
+alias id "cotransitive" = "cic:/matita/higher_order_defs/relations/cotransitive.con".
+alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con".