fact: Definition concat m1 m2 := match m1, m2 with | Leaf _, _ => m2 | _ , Leaf _ => m1 | _, Node _ l2 x2 d2 r2 => let (m2',xd) := remove_min l2 x2 d2 r2 in join m1 xd#1 xd#2 m2' end.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)