proposition: Theorem Zslice_slice : forall n k1 k2 k1' k2', (0 <= k1' <= k2)%Z -> Zslice (Zslice n k1 k2) k1' k2' = Zslice n (k1 + k1') (Z.min (k2 - k1') k2').
proof: Proof. intros n k1 k2 k1' k2' Hk1'. destruct (Zle_or_lt 0 k2') as [Hk2'|Hk2']. apply Zdigit_ext. intros k Hk. destruct (Zle_or_lt (Z.min (k2 - k1') k2') k) as [Hk'|Hk']. rewrite (Zdigit_slice_out n (k1 + k1')) with (1 := Hk'). destruct (Zle_or_lt k2' k) as [Hk''|Hk'']. now apply Zdigit_slice_out. rewrite Zdigit_slice by now split. apply Zdigit_slice_out. lia. rewrite Zdigit_slice by lia. rewrite (Zdigit_slice n (k1 + k1')) by now split. rewrite Zdigit_slice. now rewrite Zplus_assoc. lia. unfold Zslice. rewrite Z.min_r. now rewrite Zle_bool_false. lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux