proposition: Lemma remove_min_bindings m m' p : RemoveMin m (m',p) -> bindings m = p :: bindings m'.
proof: Proof. revert m'. induction m as [|h l IH x e r _]; [destruct 1|]. intros m' R. apply RemoveMin_step in R. destruct R as [(->,(->,->))|[m0 (R,->)]]; auto. rewrite bal_bindings, create_bindings, bindings_node. now rewrite (IH _ R). Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)