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