proposition: Theorem Zdigits_unique : forall n d, (Zpower beta (d - 1) <= Z.abs n < Zpower beta d)%Z -> Zdigits n = d.
proof: Proof. intros n d Hd. assert (Hd' := Zdigits_correct n). apply Zle_antisym. apply (Zpower_lt_Zpower beta). now apply Z.le_lt_trans with (Z.abs n). apply (Zpower_lt_Zpower beta). now apply Z.le_lt_trans with (Z.abs n). Qed.
imports: Coq(Lia ZArith Zquot) Zaux