proposition: Theorem Zsame_sign_scale : forall n k, (0 <= n * Zscale n k)%Z.
proof: Proof. intros n k. unfold Zscale. case Zle_bool_spec ; intros Hk. rewrite Zmult_assoc. apply Zmult_le_0_compat. apply Zsame_sign_imp ; apply Zlt_le_weak. apply Zpower_ge_0. apply Zsame_sign_odiv. apply Zpower_ge_0. Qed.
imports: Coq(Lia ZArith Zquot) Zaux