proposition: Lemma mapo_find m x `{!Ok m} : exists y, y == x /\ find x (mapo f m) = obind (find x m) (f y).
proof: Proof. functional induction (mapo f m); simpl; auto; invok. - now exists x. - rewrite join_find; auto. + simpl. case K.compare_spec; simpl; intros. * now exists x0. * destruct IHt0 as (y' & ? & ?); auto. exists y'; split; trivial. * destruct IHt1 as (y' & ? & ?); auto. exists y'; split; trivial. + constructor; chok; auto using mapo_lt, mapo_gt with *. - rewrite concat_find; autok. + destruct IHt1 as (y' & ? & ->); auto. destruct IHt0 as (y'' & ? & ->); auto. case K.compare_spec; simpl; intros. * nonify (find x r). nonify (find x l). simpl. now exists x0. * nonify (find x r). now exists y''. * nonify (find x l). exists y'. split; trivial. destruct (find x r); simpl; trivial. now destruct (f y' e). + apply between with x0; autom. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)