fact: Fixpoint partition (f:elt->bool)(s : t) : t*t := match s with | Leaf => (Leaf, Leaf) | Node _ l x r => let (l1,l2) := partition f l in let (r1,r2) := partition f r in if f x then (join l1 x r1, concat l2 r2) else (concat l1 r1, join l2 x r2) end.
imports: FunInd MSetInterface MSetGenTree BinInt Int