proposition: Theorem Zslice_scale : forall n k k1 k2, (0 <= k1)%Z -> Zslice (Zscale n k) k1 k2 = Zslice n (k1 - k) k2.
proof: Proof. intros n k k1 k2 Hk1. unfold Zscale. case Zle_bool_spec; intros Hk. now apply Zslice_mul_pow. apply Zslice_div_pow with (2 := Hk1). lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux