proposition: Lemma radix_to_pos (r : radix) : Z.pos (Z.to_pos r) = r.
proof: Proof. now destruct r as [[]]. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic