proposition: Lemma even_radix_correct : forall beta, match radix_val beta with Zpos (xO _) => true | _ => false end = Z.even beta.
proof: Proof. intros (beta, Hb). revert Hb. case beta ; try easy. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic