proposition: Theorem Zpower_gt_Zdigits : forall e x, (Zdigits x <= e)%Z -> (Z.abs x < Zpower beta e)%Z.
proof: Proof. intros e x Hex. destruct (Zdigits_correct x) as [H1 H2]. apply Z.lt_le_trans with (1 := H2). now apply Zpower_le. Qed.
imports: Coq(Lia ZArith Zquot) Zaux