proposition: Lemma le_lt_trans x y z : x ≤ y → y < z → x < z.
proof: Proof. rewrite !lt_iff_le_apart. intros E2 [E1a E1b]. split. now transitivity y. destruct (cotransitive E1b x) 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