proposition: Theorem Zdigit_slice : forall n k1 k2 k, (0 <= k < k2)%Z -> Zdigit (Zslice n k1 k2) k = Zdigit n (k1 + k).
proof: Proof. intros n k1 k2 k Hk. unfold Zslice. rewrite Zle_bool_true. rewrite Zdigit_mod_pow by apply Hk. rewrite Zdigit_scale by apply Hk. unfold Zminus. now rewrite Z.opp_involutive, Zplus_comm. lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux