fact: Fixpoint split x s : triple := match s with | Leaf => << Leaf, false, Leaf >> | Node _ l y r => match X.compare x y with | Lt => let (ll,b,rl) := split x l in << ll, b, join rl y r >> | Eq => << l, true, r >> | Gt => let (rl,b,rr) := split x r in << join l y rl, b, rr >> end end.
imports: FunInd MSetInterface MSetGenTree BinInt Int