fact: Fixpoint remove (k : key) (s : t elt) : t elt := match s with | nil => nil | (k',x) :: l => match X.compare k k' with | Lt => s | Eq => l | Gt => (k',x) :: remove k l end end.
imports: Coq(OrdersFacts OrdersLists)