proposition: Lemma remove_min_gt m m' p `{!Ok m} : RemoveMin m (m',p) -> p#1 < m'.
proof: Proof. revert m'. induction m as [|h l IH x e r _]; [destruct 1|]. intros m' R. invok. apply RemoveMin_step in R. destruct R as [(_,(->,->))|[m0 (R,->)]]; auto. assert (p#1 < m0) by now apply IH. assert (p#1 ∈ l) by (apply (remove_min_in R); now left). intros z. rewrite bal_in. intuition; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)