proposition: Lemma ins_above m x v y : m < y -> x < y -> ins x v m < y.
proof: Proof. intros. treeorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)