proposition: Lemma split_in_2 : forall m x, bst m -> forall y, (In y (split x m)#r <-> In y m /\ X.lt x y).
proof: Proof. intros m x; functional induction (split x m); subst; simpl; intros; inv bst; try clear e0. - intuition_in. - rewrite join_in. rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. - intuition_in; order. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int