proposition: Lemma digits2_digits : forall m : positive, Zpos (digits m) = Zdigits radix2 (Zpos m).
proof: Proof. intros m. apply trans_eq with (Z_of_nat (S (digits2_Pnat m))). induction m ; simpl. now rewrite 2!Zpos_succ_morphism, IHm. now rewrite 2!Zpos_succ_morphism, IHm. easy. rewrite Zdigits_mag. 2: easy. apply sym_eq. apply mag_unique. generalize (digits2_Pnat_correct m). generalize (digits2_Pnat m). intros d H. simpl in H. replace (Z_of_nat (S d) - 1)%Z with (Z_of_nat d). rewrite <- abs_IZR. rewrite <- 2!IZR_Zpower_nat. split. now apply IZR_le. now apply IZR_lt. rewrite inj_S. apply Zpred_succ. Qed.
imports: Coq(ZArith Reals) Flocq(Zaux Raux Defs Digits Float_prop Generic_fmt FIX FLX) Gappa_definitions Gappa_dyadic