fact: Fixpoint partition (f : elt -> bool) (s : t) : t * t := match s with | nil => (nil, nil) | x :: l => let (s1, s2) := partition f l in if f x then (x :: s1, s2) else (s1, x :: s2) end.
imports: MSetInterface OrdersFacts OrdersLists