proposition: Lemma join_find l x d r y : Ok (create l x d r) -> find y (join l x d r) = find y (create l x d r).
proof: Proof. unfold create at 1. join_tac l x d r; trivial. - simpl in *. invok. rewrite add_find; trivial. case K.compare_spec; intros; trivial. apply not_find_iff; auto. intro. order. - clear Hlr. factornode l. simpl. invok. rewrite add_find by auto. case K.compare_spec; intros; trivial. apply not_find_iff; auto. intro. order. - clear Hrl LT. factornode r. invok; invlt; rewrite bal_find; autok; simpl. + rewrite Hlr by (ok; intuition). simpl. do 2 (case K.compare_spec; intuition; try order). + apply join_ok, create_ok; ok; intuition. + intro. rewrite join_in. intuition; order. - clear Hlr LT LT'. factornode l. invok; invlt; rewrite bal_find; autok; simpl. + rewrite Hrl by (ok; intuition). simpl. do 2 (case K.compare_spec; intuition; try order). + apply join_ok, create_ok; ok; intuition. + intro. rewrite join_in. intuition; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)