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