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