proposition: Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
proof: Proof. Proof with auto with ordered_type. intros x y z H ?; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H); apply eq_trans with z... - elim (lt_not_eq (lt_trans Hlt H))... Qed.
imports: SetoidList Morphisms OrdersTac