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