proposition: Theorem Zdigit_not_0_pos : forall e n, (0 <= e)%Z -> (Zpower beta e <= n < Zpower beta (e + 1))%Z -> Zdigit n e <> Z0.
proof: Proof. intros e n He (Hn1,Hn2). unfold Zdigit. rewrite <- ZOdiv_mod_mult. rewrite Z.rem_small. intros H. apply Zle_not_lt with (1 := Hn1). rewrite (Z.quot_rem' n (beta ^ e)). rewrite H, Zmult_0_r, Zplus_0_l. apply Zrem_lt_pos_pos. apply Z.le_trans with (2 := Hn1). apply Zpower_ge_0. now apply Zpower_gt_0. split. apply Z.le_trans with (2 := Hn1). apply Zpower_ge_0. replace (beta ^ e * beta)%Z with (beta ^ (e + 1))%Z. exact Hn2. rewrite <- (Zmult_1_r beta) at 3. now apply (Zpower_plus beta e 1). Qed.
imports: Coq(Lia ZArith Zquot) Zaux