proposition: Theorem Zslice_div_pow_scale : forall n k k1 k2, (0 <= k)%Z -> Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
proof: Proof. intros n k k1 k2 Hk. apply Zdigit_ext. intros k' Hk'. rewrite Zdigit_scale with (1 := Hk'). unfold Zminus. rewrite (Zplus_comm k'), Z.opp_involutive. destruct (Zle_or_lt k2 k') as [Hk2|Hk2]. rewrite Zdigit_slice_out with (1 := Hk2). apply sym_eq. apply Zdigit_slice_out. now apply Zplus_le_compat_l. rewrite Zdigit_slice by now split. destruct (Zle_or_lt 0 (k1 + k')) as [Hk1'|Hk1']. rewrite Zdigit_slice by lia. rewrite Zdigit_div_pow by assumption. apply f_equal. ring. now rewrite 2!Zdigit_lt. Qed.
imports: Coq(Lia ZArith Zquot) Zaux