proposition: Theorem Zdigits_Zpower : forall e, (0 <= e)%Z -> Zdigits (Zpower beta e) = (e + 1)%Z.
proof: Proof. intros e He. rewrite <- (Zmult_1_l (Zpower beta e)). rewrite Zdigits_mult_Zpower ; try easy. apply Zplus_comm. Qed.
imports: Coq(Lia ZArith Zquot) Zaux