proposition: Lemma split_find : forall m x y, bst m -> find y m = match X.compare y x with | LT _ => find y (split x m)#l | EQ _ => (split x m)#o | GT _ => find y (split x m)#r end.
proof: Proof. intros m x; functional induction (split x m); subst; simpl; intros; inv bst; try clear e0; try rewrite e1 in *; simpl in *; [ destruct X.compare; auto | .. ]; try match goal with E:split ?x ?t = _, B:bst ?t |- _ => generalize (split_in_1 x B)(split_in_2 x B)(split_bst x B); rewrite E; simpl; destruct 3 end. - rewrite join_find, IHt; auto; clear IHt; simpl. + repeat (destruct X.compare; auto); order. + intro y1; rewrite H4; intuition. - repeat (destruct X.compare; auto); order. - rewrite join_find, IHt; auto; clear IHt; simpl. + repeat (destruct X.compare; auto); order. + intros y1; rewrite H; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int