proposition: Theorem Zscale_mul_pow : forall n k k', (0 <= k)%Z -> Zscale (n * Zpower beta k) k' = Zscale n (k + k').
proof: Proof. intros n k k' Hk. unfold Zscale. case Zle_bool_spec ; intros Hk'. rewrite Zle_bool_true. rewrite <- Zmult_assoc. apply f_equal. now rewrite Zpower_plus. now apply Zplus_le_0_compat. case Zle_bool_spec ; intros Hk''. pattern k at 1 ; replace k with (k + k' + -k')%Z by ring. assert (0 <= -k')%Z by lia. rewrite Zpower_plus by easy. rewrite Zmult_assoc, Z_quot_mult. apply refl_equal. apply Zgt_not_eq. now apply Zpower_gt_0. replace (-k')%Z with (-(k+k') + k)%Z by ring. rewrite Zpower_plus with (2 := Hk). apply Zquot_mult_cancel_r. apply Zgt_not_eq. now apply Zpower_gt_0. lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux