+
+lemma lt_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z < y → z < x.
+intros (A x y z E H); split; elim H;
+[apply (le_rewr ???? (eq_sym ??? E));|apply (ap_rewr ???? E)] assumption;
+qed.
+
+lemma lt_rewl: ∀A:excedence.∀x,z,y:A. x ≈ y → y < z → x < z.
+intros (A x y z E H); split; elim H;
+[apply (le_rewl ???? (eq_sym ??? E));| apply (ap_rewl ???? E);] assumption;
+qed.
+
+lemma lt_le_transitive: ∀A:excedence.∀x,y,z:A.x < y → y ≤ z → x < z.
+intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)]
+whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)]
+cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)]
+right; assumption;
+qed.
+
+lemma le_lt_transitive: ∀A:excedence.∀x,y,z:A.x ≤ y → y < z → x < z.
+intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)]
+whd in LE LEx APx; cases APx (EXx EXx); [cases (LEx EXx)]
+cases (exc_cotransitive ??? x EXx) (EXz EXz); [right; assumption]
+cases LE; assumption;
+qed.
+
+lemma le_le_eq: ∀E:excedence.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
+intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
+qed.
+
+lemma eq_le_le: ∀E:excedence.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a.
+intros (E x y H); unfold apart_of_excedence in H; unfold apart in H;
+simplify in H; split; intro; apply H; [left|right] assumption.
+qed.
+
+lemma ap_le_to_lt: ∀E:excedence.∀a,c:E.c # a → c ≤ a → c < a.
+intros; split; assumption;
+qed.
+
+definition total_order_property : ∀E:excedence. Type ≝
+ λE:excedence. ∀a,b:E. a ≰ b → b < a.
+