proposition: Theorem Zdigit_not_0 : forall e n, (0 <= e)%Z -> (Zpower beta e <= Z.abs n < Zpower beta (e + 1))%Z -> Zdigit n e <> Z0.
proof: Proof. intros e n He Hn. destruct (Zle_or_lt 0 n) as [Hn'|Hn']. rewrite (Z.abs_eq _ Hn') in Hn. now apply Zdigit_not_0_pos. intros H. rewrite (Zabs_non_eq n) in Hn by now apply Zlt_le_weak. apply (Zdigit_not_0_pos _ _ He Hn). now rewrite Zdigit_opp, H. Qed.
imports: Coq(Lia ZArith Zquot) Zaux