proposition: Lemma remove_min_mapsto m m' p : RemoveMin m (m',p) -> forall y e, MapsTo y e m <-> (y == p#1 /\ e = p#2) \/ MapsTo y e m'.
proof: Proof. revert m'. induction m as [|h l IH x d r _]; [destruct 1|]. intros m' R. apply RemoveMin_step in R. destruct R as [(->,(->,->))|[m0 (R,->)]]; intros y e; simpl. - intuition_m. subst. now constructor. - rewrite bal_mapsto. unfold create. specialize (IH _ R y e). intuition_m. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)