proposition: Lemma split_bst : forall m x, bst m -> bst (split x m)#l /\ bst (split x m)#r.
proof: Proof. intros m x; functional induction (split x m); subst; simpl; intros; inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition; apply join_bst; auto. - intros y0. generalize (split_in_2 x H0 y0); rewrite e1; simpl; intuition. - intros y0. generalize (split_in_1 x H1 y0); rewrite e1; simpl; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int