lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
intros (A x z y Exy Ayz); cases (exc_cotransitive ?? x Ayz); [2:assumption]
lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z.
intros (A x z y Exy Ayz); cases (exc_cotransitive ?? x Ayz); [2:assumption]