StrictOrder (<). Proof. split. - apply _. - intros x E. apply lt_correct in E. destruct E as [_ []];trivial. - intros x y z E1 E2. apply lt_correct; apply lt_correct in E1; apply lt_correct in E2. destruct E1 as [E1a E1b],E2 as [E2a E2b]. split. + transitivity y;trivial. + intros E3. destruct E2b. apply (antisymmetry (≤)); trivial. rewrite <-E3. assumption. Qed.
Require Import