proposition: Lemma seqZ_app m n1 n2 : 0 ≤ n1 → 0 ≤ n2 → seqZ m (n1 + n2) = seqZ m n1 ++ seqZ (m + n1) n2.
proof: Proof. intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done. f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose. apply list_fmap_ext; intros j n; simpl. rewrite Nat2Z.inj_add, Z2Nat.id by done. lia. Qed.
imports: stdpp(options)