proposition: Theorem Zdigit_slice_out : forall n k1 k2 k, (k2 <= k)%Z -> Zdigit (Zslice n k1 k2) k = Z0.
proof: Proof. intros n k1 k2 k Hk. unfold Zslice. case Zle_bool_spec ; intros Hk2. apply Zdigit_mod_pow_out. now split. apply Zdigit_0. Qed.
imports: Coq(Lia ZArith Zquot) Zaux