x y z : x ≤ y -> y < z -> x < z. Proof. intros E2 E1. apply lt_iff_le_apart. apply lt_iff_le_apart in E1. destruct E1 as [E1a E1b]. split. - transitivity y;auto. - apply (merely_destruct (cotransitive E1b x));intros [E3 | E3]; trivial. apply lt_apart. apply symmetry in E3. transitivity y; apply lt_iff_le_apart; auto. Qed.
Require Import