proposition: Lemma pseudo_order_lt_ext x₁ y₁ x₂ y₂ : x₁ < y₁ -> merely (x₂ < y₂ |_| x₁ ≶ x₂ |_| y₂ ≶ y₁).
proof: Proof. intros E. apply (merely_destruct (pseudo_order_cotrans_twice x₁ y₁ x₂ y₂ E)); intros [?|[?|?]];apply tr; auto using pseudo_order_lt_apart. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness