proposition: Theorem Zscale_scale : forall n k k', (0 <= k)%Z -> Zscale (Zscale n k) k' = Zscale n (k + k').
proof: Proof. intros n k k' Hk. unfold Zscale at 2. rewrite Zle_bool_true with (1 := Hk). now apply Zscale_mul_pow. Qed.
imports: Coq(Lia ZArith Zquot) Zaux