proposition: Theorem Zplus_slice : forall n k l1 l2, (0 <= l1)%Z -> (0 <= l2)%Z -> (Zslice n k l1 + Zscale (Zslice n (k + l1) l2) l1)%Z = Zslice n k (l1 + l2).
proof: Proof. intros n k1 l1 l2 Hl1 Hl2. clear Hl1. apply Zdigit_ext. intros k Hk. rewrite Zdigit_plus. rewrite Zdigit_scale with (1 := Hk). destruct (Zle_or_lt (l1 + l2) k) as [Hk2|Hk2]. rewrite Zdigit_slice_out with (1 := Hk2). now rewrite 2!Zdigit_slice_out by lia. rewrite Zdigit_slice with (1 := conj Hk Hk2). destruct (Zle_or_lt l1 k) as [Hk1|Hk1]. rewrite Zdigit_slice_out with (1 := Hk1). rewrite Zdigit_slice by lia. simpl ; apply f_equal. ring. rewrite Zdigit_slice with (1 := conj Hk Hk1). rewrite (Zdigit_lt _ (k - l1)) by lia. apply Zplus_0_r. rewrite Zmult_comm. apply Zsame_sign_trans_weak with n. intros H ; rewrite H. apply Zslice_0. rewrite Zmult_comm. apply Zsame_sign_trans_weak with (Zslice n (k1 + l1) l2). intros H ; rewrite H. apply Zscale_0. apply Zsame_sign_slice. apply Zsame_sign_scale. apply Zsame_sign_slice. clear k Hk ; intros k Hk. rewrite Zdigit_scale with (1 := Hk). destruct (Zle_or_lt l1 k) as [Hk1|Hk1]. left. now apply Zdigit_slice_out. right. apply Zdigit_lt. lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux