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