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