proposition: Lemma remove_min_in m m' p : RemoveMin m (m',p) -> forall y, y ∈ m <-> y == p#1 \/ y ∈ m'.
proof: Proof. intros H y. unfold In. assert (H' := remove_min_mapsto H y). firstorder. exists (p#2). rewrite H'. now left. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)