fact: Fixpoint delmin l x r : (elt * tree) := match l with | Leaf => (x,r) | Node lc ll lx lr => let (k,l') := delmin ll lx lr in match lc with | Black => (k, lbalS l' x r) | Red => (k, Rd l' x r) end end.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat