fact: Fixpoint cardinal (s : tree) : nat := match s with | Leaf => 0 | Node _ l _ _ r => S (cardinal l + cardinal r) end.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)