fact: Definition node (l : t A) (o: option A) (r : t A) : t A := match o,l,r with | None,Leaf,Leaf => Leaf | _,_,_ => Node l o r end.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)