proposition: Theorem Zsame_sign_slice : forall n k k', (0 <= n * Zslice n k k')%Z.
proof: Proof. intros n k k'. unfold Zslice. case Zle_bool. apply Zsame_sign_trans_weak with (Zscale n (-k)). intros H ; rewrite H. apply Zrem_0_l. apply Zsame_sign_scale. rewrite Zmult_comm. apply Zrem_sgn2. now rewrite Zmult_0_r. Qed.
imports: Coq(Lia ZArith Zquot) Zaux