fact: Fixpoint remove (i : elt) (m : t) {struct m} : t := match m with | Leaf => Leaf | Node l o r => match i with | 1 => node l false r | i~0 => node (remove i l) o r | i~1 => node l o (remove i r) end end.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface