proposition: Lemma split_in_3 : forall m x, bst m -> (split x m)#o = find x m.
proof: Proof. intros m x; functional induction (split x m); subst; simpl; auto; intros; inv bst; try clear e0; destruct X.compare; try order; trivial; rewrite <- IHt, e1; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int