proposition: Lemma concat_bindings m1 m2 `{!Ok m1, !Ok m2} : m1 < m2 -> bindings (concat m1 m2) = bindings m1 ++ bindings m2.
proof: Proof. functional induction (concat m1 m2); intros B; auto; try factornode m1. - symmetry. apply app_nil_r. - factor_remove_min m2 R. assert (m1 < xd#1). { intros z Hz. apply B; trivial. rewrite (remove_min_in R). now left. } rewrite join_bindings, create_bindings. + f_equal. rewrite (remove_min_bindings R). f_equal. now destruct xd. + 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)