proposition: Theorem Zdigits_mag : forall n, n <> Z0 -> Zdigits beta n = mag beta (IZR n).
proof: Proof. intros n Hn. destruct (mag beta (IZR n)) as (e, He) ; simpl. specialize (He (IZR_neq _ _ Hn)). rewrite <- abs_IZR in He. assert (Hd := Zdigits_correct beta n). assert (Hd' := Zdigits_gt_0 beta n). apply Zle_antisym ; apply (bpow_lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). rewrite <- IZR_Zpower by lia. now apply IZR_le. apply Rle_lt_trans with (1 := proj1 He). rewrite <- IZR_Zpower by lia. now apply IZR_lt. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits