fact: Fixpoint cardinal (m : t) : nat := match m with | Leaf => O | Node l false r => (cardinal l + cardinal r)%nat | Node l true r => S (cardinal l + cardinal r) end.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface