x₁ y₁ x₂ y₂ : x₁ < y₁ -> merely (x₂ < y₂ |_| x₁ ≶ x₂ |_| y₂ ≶ y₁). 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.
Require Import