proposition: Lemma le_lt_trans x y z : x ≤ y -> y < z -> x < z.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness