proposition: Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
proof: Proof. induction s as [|x s IH]; intros [|x' s']; simpl; intuition auto with relations. elim_compare x x'; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists