proposition: Theorem Zdigit_div_pow : forall n k k', (0 <= k)%Z -> (0 <= k')%Z -> Zdigit (Z.quot n (Zpower beta k')) k = Zdigit n (k + k').
proof: Proof. intros n k k' Hk Hk'. unfold Zdigit. rewrite Zquot_Zquot. rewrite Zplus_comm. now rewrite Zpower_plus. Qed.
imports: Coq(Lia ZArith Zquot) Zaux