proposition: Theorem Zdigit_mod_pow : forall n k k', (k < k')%Z -> Zdigit (Z.rem n (Zpower beta k')) k = Zdigit n k.
proof: Proof. intros n k k' Hk. destruct (Zle_or_lt 0 k) as [H|H]. unfold Zdigit. rewrite <- 2!ZOdiv_mod_mult. apply (f_equal (fun x => Z.quot x (beta ^ k))). replace k' with (k + 1 + (k' - (k + 1)))%Z by ring. rewrite Zpower_exp by lia. rewrite Zmult_comm. rewrite Zpower_plus by easy. change (Zpower beta 1) with (beta * 1)%Z. rewrite Zmult_1_r. apply ZOmod_mod_mult. now rewrite 2!Zdigit_lt. Qed.
imports: Coq(Lia ZArith Zquot) Zaux