fact: Fixpoint split x m : triple := match m with | Leaf => << Leaf, None, Leaf >> | Node l y d r h => match X.compare x y with | LT _ => let (ll,o,rl) := split x l in << ll, o, join rl y d r >> | EQ _ => << l, Some d, r >> | GT _ => let (rl,o,rr) := split x r in << join l y d rl, o, rr >> end end.
imports: FunInd FMapInterface FMapList ZArith Int