proposition: Lemma join_find : forall l x d r y, bst l -> bst r -> lt_tree x l -> gt_tree x r -> find y (join l x d r) = find y (create l x d r).
proof: Proof. join_tac; auto; inv bst; simpl (join (Leaf elt)); try (assert (X.lt lx x) by auto with ordered_type); try (assert (X.lt x rx) by auto with ordered_type); rewrite ?add_find, ?bal_find; auto. - simpl; destruct X.compare; auto. rewrite not_find_iff; auto; intro; order. - simpl; repeat (destruct X.compare; auto); try (order; fail). rewrite not_find_iff by auto; intro. assert (X.lt y x) by auto; order. - simpl; rewrite Hlr; simpl; auto. repeat (destruct X.compare; auto); order. - intros u Hu; rewrite join_in in Hu. destruct Hu as [Hu|[Hu|Hu]]; try generalize (H2 _ Hu); order. - simpl; rewrite Hrl; simpl; auto. repeat (destruct X.compare; auto); order. - intros u Hu; rewrite join_in in Hu. destruct Hu as [Hu|[Hu|Hu]]; order. Qed.
imports: FunInd FMapInterface FMapList ZArith Int