proposition: Theorem Zdigits_div_Zpower : forall m e, (0 <= m)%Z -> (0 <= e <= Zdigits m)%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. destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He']. rewrite Z.abs_eq in H by easy. destruct H as [H1 H2]. rewrite Z.abs_eq. split. replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring. rewrite Z.pow_sub_r. 2: apply Zgt_not_eq, radix_gt_0. 2: clear -He He' ; lia. apply Z_div_le with (2 := H1). now apply Z.lt_gt, Zpower_gt_0. apply Zmult_lt_reg_r with (Zpower beta e). now apply Zpower_gt_0. apply Z.le_lt_trans with m. rewrite Zmult_comm. apply Z_mult_div_ge. now apply Z.lt_gt, Zpower_gt_0. rewrite <- Zpower_plus. now replace (Zdigits m - e + e)%Z with (Zdigits m) by ring. now apply Zle_minus_le_0. apply He. apply Z_div_pos with (2 := Hm). now apply Z.lt_gt, Zpower_gt_0. rewrite He'. rewrite (Zeq_minus _ (Zdigits m)) by reflexivity. simpl. rewrite Zdiv_small. easy. split. exact Hm. now rewrite <- (Z.abs_eq m) at 1. Qed.
imports: Coq(Lia ZArith Zquot) Zaux