proposition: Lemma remove_lt m x y `{!Ok m} : m < y -> remove x m < y.
proof: Proof. intros ? z. rewrite remove_in by trivial. destruct 1; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)