fact: Fixpoint find (k:key) (m: t elt) : option elt := match m with | nil => None | (k',x)::m' => match X.compare k k' with | Lt => None | Eq => Some x | Gt => find k m' end end.
imports: Coq(OrdersFacts OrdersLists)