x₁ y₁ x₂ y₂ : x₁ < y₁ -> merely (x₂ < y₂ |_| x₁ < x₂ |_| y₂ < y₁). Proof. intros E1. apply (merely_destruct (cotransitive E1 x₂));intros [?|E2]; try solve [apply tr;auto]. apply (merely_destruct (cotransitive E2 y₂));intros [?|?];apply tr;auto. Qed.
Require Import