proposition: Theorem Zdigit_mul_pow : forall n k k', (0 <= k')%Z -> Zdigit (n * Zpower beta k') k = Zdigit n (k - k').
proof: Proof. intros n k k' Hk'. destruct (Zle_or_lt k' k) as [H|H]. revert k H. pattern k' ; apply Zlt_0_ind with (2 := Hk'). clear k' Hk'. intros k' IHk' Hk' k H. unfold Zdigit. apply (f_equal (fun x => Z.rem x beta)). pattern k at 1 ; replace k with (k - k' + k')%Z by ring. rewrite Zpower_plus with (2 := Hk'). apply Zquot_mult_cancel_r. apply Zgt_not_eq. now apply Zpower_gt_0. now apply Zle_minus_le_0. destruct (Zle_or_lt 0 k) as [H0|H0]. rewrite (Zdigit_lt n) by lia. unfold Zdigit. replace k' with (k' - k + k)%Z by ring. rewrite Zpower_plus with (2 := H0). rewrite Zmult_assoc, Z_quot_mult. replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring. rewrite Zpower_exp by lia. rewrite Zmult_assoc. change (Zpower beta 1) with (beta * 1)%Z. rewrite Zmult_1_r. apply Z_rem_mult. apply Zgt_not_eq. now apply Zpower_gt_0. apply Zle_minus_le_0. now apply Zlt_le_weak. rewrite Zdigit_lt with (1 := H0). apply sym_eq. apply Zdigit_lt. lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux