proposition: Theorem Zdigit_ge_Zpower : forall e n, (Z.abs n < Zpower beta e)%Z -> forall k, (e <= k)%Z -> Zdigit n k = Z0.
proof: Proof. intros e [|n|n] Hn k. easy. apply Zdigit_ge_Zpower_pos. now split. intros He. change (Zneg n) with (Z.opp (Zpos n)). rewrite Zdigit_opp. rewrite Zdigit_ge_Zpower_pos with (2 := He). apply Z.opp_0. now split. Qed.
imports: Coq(Lia ZArith Zquot) Zaux