  Most existing implementations of multiple precision arithmetic demand that
the user sets the precision {\em a priori}. Some libraries are said adaptable
in the sense that they dynamically change the precision of each intermediate
operation individually to deliver the target accuracy according to the actual
inputs. We present in this text a new adaptable numeric core inspired both from
floating point expansions and from on-line arithmetic.
  The numeric core is cut down to four tools. The tool that contains arithmetic
operations is proved to be correct. The proofs have been formally checked by
the Coq assistant. Developing the proofs, we have formally proved many results
published in the literature and we have extended a few of them. This work may
let users (i) develop application specific adaptable libraries based on the
toolset and / or (ii) write new formal proofs based on the set of validated
facts.
