proposition: Theorem Zdigits_slice : forall n k l, (0 <= l)%Z -> (Zdigits (Zslice n k l) <= l)%Z.
proof: Proof. intros n k l Hl. unfold Zslice. rewrite Zle_bool_true with (1 := Hl). destruct (Zdigits_correct (Z.rem (Zscale n (- k)) (Zpower beta l))) as (H1,H2). apply Zpower_lt_Zpower with beta. apply Z.le_lt_trans with (1 := H1). rewrite <- (Z.abs_eq (beta ^ l)) at 2 by apply Zpower_ge_0. apply Zrem_lt. apply Zgt_not_eq. now apply Zpower_gt_0. Qed.
imports: Coq(Lia ZArith Zquot) Zaux