proposition: Lemma lt_le_trans x y z : x < y → y ≤ z → x < z.
proof: Proof. rewrite !lt_iff_le_apart. intros [E1a E1b] E2. split. now transitivity y. destruct (cotransitive E1b z) as [E3 | E3]; trivial. apply lt_apart. symmetry in E3. transitivity y; rewrite lt_iff_le_apart; tauto. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids