fact: Fixpoint min_elt (m: t) : option elt := match m with | Leaf => None | Node l o r => match min_elt l with | None => if o then Some 1 else option_map xI (min_elt r) | Some i => Some i~0 end end.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface