proposition: Lemma add_lt m x e y : m < y -> x < y -> add x e m < y.
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)