FullPseudoOrder (≤) (<). Proof. split; try apply _. intros x y. split. - intros ? E. apply lt_correct in E;destruct E as [? []]. apply (antisymmetry (≤));assumption. - intros E1. destruct (total (≤) x y); trivial. destruct (dec (x = y)) as [E2|E2]. + rewrite E2. apply reflexivity. + destruct E1. apply lt_correct;split;auto. apply symmetric_neq;assumption. Qed.
Require Import