proposition: Lemma remove_min_lt m m' p : RemoveMin m (m',p) -> forall y, m < y -> m' < y.
proof: Proof. intros R y L z Hz. apply L. apply (remove_min_in R). now right. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)