proposition: Theorem Zslice_div_pow : forall n k k1 k2, (0 <= k)%Z -> (0 <= k1)%Z -> Zslice (Z.quot n (Zpower beta k)) k1 k2 = Zslice n (k1 + k) k2.
proof: Proof. intros n k k1 k2 Hk Hk1. unfold Zslice. case Zle_bool_spec ; intros Hk2. 2: apply refl_equal. apply (f_equal (fun x => Z.rem x (beta ^ k2))). unfold Zscale. case Zle_bool_spec ; intros Hk1'. replace k1 with Z0 by lia. case Zle_bool_spec ; intros Hk'. replace k with Z0 by lia. simpl. now rewrite Z.quot_1_r. rewrite Z.opp_involutive. apply Zmult_1_r. rewrite Zle_bool_false by lia. rewrite 2!Z.opp_involutive, Zplus_comm. rewrite Zpower_plus by assumption. apply Zquot_Zquot. Qed.
imports: Coq(Lia ZArith Zquot) Zaux