proposition: Lemma le_lt_trans (a b c: A): le a b -> lt b c -> lt a c.
proof: Proof. intros Hle_ab Hlt_bc. apply le_lt_eq in Hle_ab as [Heq_ab | Hlt_ab]. - now transitivity b. - now subst. Qed.
imports: Coq(Relations RelationClasses Setoid)