proposition: Lemma lt_nlt_trans {x y z : A} : x < y -> ~ (z < y) -> x < z.
proof: Proof. intros ltxy nltzy. assert (disj := cotransitive ltxy z). strip_truncations. destruct disj as [ltxz|ltzy]. - exact ltxz. - destruct (nltzy ltzy). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness