fact: Definition convert_location_inv l := match l with | pos_Eq => loc_Exact | pos_Lo => loc_Inexact Lt | pos_Mi => loc_Inexact Eq | pos_Up => loc_Inexact Gt end.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic