proposition: Lemma digits_conversion : forall beta p, Zdigits beta (Zpos p) = Zpos (count_digits beta p).
proof: Proof. intros beta p. unfold Zdigits, count_digits. generalize xH, (radix_val beta), p at 1 3. induction p ; simpl ; intros. case (Zlt_bool (Zpos p1) z). apply refl_equal. rewrite <- IHp. now rewrite Pplus_one_succ_r. case (Zlt_bool (Zpos p1) z). apply refl_equal. rewrite <- IHp. now rewrite Pplus_one_succ_r. now case (Zlt_bool (Zpos p0) z). Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic