proposition: Theorem Zslice_mul_pow : forall n k k1 k2, (0 <= k)%Z -> Zslice (n * Zpower beta k) k1 k2 = Zslice n (k1 - k) k2.
proof: Proof. intros n k k1 k2 Hk. unfold Zslice. case Zle_bool_spec ; intros Hk2. 2: apply refl_equal. rewrite Zscale_mul_pow with (1 := Hk). now replace (- (k1 - k))%Z with (k + -k1)%Z by ring. Qed.
imports: Coq(Lia ZArith Zquot) Zaux