proposition: Lemma lt_transitive : Transitive (_ : Lt A).
proof: Proof. intros x y z ltxy ltyz. assert (ltxyz := cotransitive ltxy z). strip_truncations. destruct ltxyz as [ltxz|ltzy]. - assumption. - destruct (pseudo_order_antisym y z (ltyz , ltzy)). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness