fact: Fixpoint xpartition (m : t) (i : positive) : t * t := match m with | Leaf => (Leaf,Leaf) | Node l o r => let (lt,lf) := xpartition l i~0 in let (rt,rf) := xpartition r i~1 in if o then let fi := f (rev i) in (node lt fi rt, node lf (negb fi) rf) else (node lt false rt, node lf false rf) end.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface