proposition: Lemma compare_spec : forall s s', Ok s -> Ok s' -> CompSpec eq lt s s' (compare s s').
proof: Proof. intros s s' Hs Hs'. destruct (compare_spec_aux s s'); constructor; auto. - exists s, s'; repeat split; auto using @ok. - exists s', s; repeat split; auto using @ok. Qed.
imports: MSetInterface OrdersFacts OrdersLists