proposition: Lemma concat_find m1 m2 y `{!Ok m1, !Ok m2} : m1 < m2 -> find y (concat m1 m2) = oelse (find y m2) (find y m1).
proof: Proof. functional induction (concat m1 m2); intros B; auto; try factornode m1. - destruct (find y m2); auto. - factor_remove_min m2 R. assert (m1 < xd#1). { intros z Hz. apply B; trivial. rewrite (remove_min_in R). now left. } rewrite join_find; simpl; auto. + rewrite (remove_min_find R y). case K.compare_spec; intros; auto. destruct (find y m2'); trivial. simpl. symmetry. apply not_find_iff; eautom. + apply create_ok; eauto with *. now apply (remove_min_gt R). Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)