proposition: Lemma fmap_add_seqZ m m' n : Z.add m <$> seqZ m' n = seqZ (m + m') n.
proof: Proof. revert m'. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m'. - by rewrite seqZ_nil. - rewrite (seqZ_cons m') by lia. rewrite (seqZ_cons (m + m')) by lia. f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia. - by rewrite !seqZ_nil by lia. Qed.
imports: stdpp(options)