+qed.
+
+lemma exc_rewl: ∀A:excedence.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
+intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption]
+cases Exy; right; assumption;
+qed.
+
+lemma exc_rewr: ∀A:excedence.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x.
+intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption]
+elim (Exy); left; assumption;
+qed.