proposition: Lemma convert_location_bij : forall l, convert_location_inv (convert_location l) = l.
proof: Proof. now destruct l as [|[| |]]. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic