proposition: Lemma add_gt m x e y : y < m -> y < x -> y < add x e m.
proof: Proof. intros ? ? z. rewrite add_in. destruct 1; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)