fact: Fixpoint compare s s' := match s, s' with | nil, nil => Eq | nil, _ => Lt | _, nil => Gt | x::s, x'::s' => match X.compare x x' with | Eq => compare s s' | Lt => Lt | Gt => Gt end end.
imports: MSetInterface OrdersFacts OrdersLists