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