Functor AvlProofs proves that trees of FMapAVL are not only
binary search trees, but moreover well-balanced ones. This is done
by proving that all operations preserve the balancing.
We then pack the previous elements in a IntMake functor
similar to the one of FMapAVL, but richer.
In final IntMake_ord functor, the compare function is
different from the one in FMapAVL: this non-structural
version is closer to the original Ocaml code.
We can implement S with balanced binary search trees.
When compared to FMapAVL, we maintain here two invariants
(bst and avl) instead of only bst, which is enough for fulfilling
the FMap interface.