proposition: Lemma pseudo_order_cotrans_twice x₁ y₁ x₂ y₂ : x₁ < y₁ → x₂ < y₂ ∨ x₁ < x₂ ∨ y₂ < y₁.
proof: Proof. intros E1. destruct (cotransitive E1 x₂) as [E2|E2]; try tauto. destruct (cotransitive E2 y₂); try tauto. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids