fact: Definition adjust_mantissa mode m pos sign := if need_change mode (match m with xO _ => true | _ => false end) pos sign then Pos.succ m else m.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic