fact: Fixpoint Normal {A} (m : t A) := match m with | Leaf => True | Node l o r => Normal l /\ Normal r /\ is_empty m = false end.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)