proposition: Theorem Zdigits_mult_Zpower : forall m e, m <> Z0 -> (0 <= e)%Z -> Zdigits (m * Zpower beta e) = (Zdigits m + e)%Z.
proof: Proof. intros m e Hm He. assert (H := Zdigits_correct m). apply Zdigits_unique. rewrite Z.abs_mul, Z.abs_pow, (Z.abs_eq beta). 2: now apply Zlt_le_weak, radix_gt_0. split. replace (Zdigits m + e - 1)%Z with (Zdigits m - 1 + e)%Z by ring. rewrite Zpower_plus with (2 := He). apply Zmult_le_compat_r. apply H. apply Zpower_ge_0. now apply Zlt_0_le_0_pred, Zdigits_gt_0. rewrite Zpower_plus with (2 := He). apply Zmult_lt_compat_r. now apply Zpower_gt_0. apply H. now apply Zlt_le_weak, Zdigits_gt_0. Qed.
imports: Coq(Lia ZArith Zquot) Zaux