PseudoOrder (<). Proof. split; try apply _. - intros x y [??]. destruct (lt_antisym x y); auto. - intros x y Exy z. destruct (trichotomy (<) x z) as [? | [Exz | Exz]];apply tr; try auto. right. rewrite <-Exz. assumption. - intros x y. transitivity (x <> y);[split;apply trivial_apart|]. split. + destruct (trichotomy (<) x y) as [?|[?|?]]; auto. intros E;contradiction E. + intros [?|?];[apply lt_ne|apply lt_ne_flip];trivial. Qed.
Require Import