Transitive (_ : Lt A). 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.
Require Import