proposition: Lemma pseudo_order_cotrans_twice x₁ y₁ x₂ y₂ : x₁ < y₁ -> merely (x₂ < y₂ |_| x₁ < x₂ |_| y₂ < y₁).
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness