fact: Definition mBFloat (p : R) := map (fun p : Z * Z => Float (fst p) (snd p)) (mProd Z Z (Z * Z) (mZlist (- pPred (vNum b)) (pPred (vNum b))) (mZlist (- dExp b) (Fexp (boundR p)))).
imports: Reals ZArith List PeanoNat Psatz