fact: Fixpoint remove_min l x d r : t*(key*elt) := match l with | Leaf => (r,(x,d)) | Node ll lx ld lr lh => let (l',m) := remove_min ll lx ld lr in (bal l' x d r, m) end.
imports: FunInd FMapInterface FMapList ZArith Int