Maps indexed by binary integers : IntMap. This library contains a data structure for finite sets implemented by an efficient structure of map (trees indexed by binary integers). It was initially developed by Jean Goubault. This user contribution used to be part of Coq Standard Library. It is now considered to be obsolete and subsumed by the new FSets/FMap library. IntMap can be now seen as a particular implementation of FMapInterface, see file FMapIntMap.
opam install coq-int-map.8.5.0