fact: Definition adjust_pos r d pos := match r with | Z0 => match pos with | pos_Eq => pos_Eq | _ => match d with xH => pos | _ => pos_Lo end end | Zneg _ => pos_Eq | Zpos _ => let (hd, mid) := match d with | xO p => (p, match pos with pos_Eq => pos_Mi | _ => pos_Up end) | xI p => (p, match pos with pos_Eq => pos_Lo | _ => pos end) | xH => (xH, pos_Eq) end in match Z.compare r (Zpos hd) with | Lt => pos_Lo | Eq => mid | Gt => pos_Up end end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic