proposition: Theorem Zdigit_ge_Zpower_pos : forall e n, (0 <= n < Zpower beta e)%Z -> forall k, (e <= k)%Z -> Zdigit n k = Z0.
proof: Proof. intros e n Hn k Hk. unfold Zdigit. rewrite Z.quot_small. apply Zrem_0_l. split. apply Hn. apply Z.lt_le_trans with (1 := proj2 Hn). replace k with (e + (k - e))%Z by ring. rewrite Zpower_plus. rewrite <- (Zmult_1_r (beta ^ e)) at 1. apply Zmult_le_compat_l. apply (Zlt_le_succ 0). apply Zpower_gt_0. now apply Zle_minus_le_0. apply Zlt_le_weak. now apply Z.le_lt_trans with n. generalize (Z.le_lt_trans _ _ _ (proj1 Hn) (proj2 Hn)). clear. now destruct e as [|e|e]. now apply Zle_minus_le_0. Qed.
imports: Coq(Lia ZArith Zquot) Zaux