fact: Fixpoint digits (m : positive) : positive := match m with | xH => xH | xI p => Pos.succ (digits p) | xO p => Pos.succ (digits p) end.
imports: Coq(ZArith Reals) Flocq(Zaux Raux Defs Digits Float_prop Generic_fmt FIX FLX) Gappa_definitions Gappa_dyadic