{x y z : A} : ~ (y < x) -> y < z -> x < z. Proof. intros nltyx ltyz. assert (disj := cotransitive ltyz x). strip_truncations. destruct disj as [ltyx|ltxz]. - destruct (nltyx ltyx). - exact ltxz. Qed.
Require Import