proposition: Lemma remove_min_find m m' p `{!Ok m} : RemoveMin m (m',p) -> forall y, find y m = match K.compare y p#1 with | Eq => Some p#2 | Lt => None | Gt => find y m' end.
proof: Proof. revert m'. induction m as [|h l IH x e r _]; [destruct 1|]. intros m' R y. invok. apply RemoveMin_step in R. destruct R as [(->,(->,->))|[m0 (R,->)]]; auto. assert (Ok m0) by now apply remove_min_ok in R. assert (p#1 < m0) by now apply remove_min_gt in R. assert (m0 < x) by now apply (remove_min_lt R). assert (p#1 ∈ l) by (apply (remove_min_in R); now left). simpl in *. rewrite (IH _ _ R), bal_find by trivial. clear IH. simpl. do 2 case K.compare_spec; trivial; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)