fact: Definition convert_location l := match l with | Bracket.loc_Exact => pos_Eq | Bracket.loc_Inexact l => match l with Lt => pos_Lo | Eq => pos_Mi | Gt => pos_Up end end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic