proposition: Lemma elim_compare_lt : forall x y : t, lt x y -> exists H : lt x y, compare x y = LT H.
proof: Proof. intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed.
imports: SetoidList Morphisms OrdersTac