Skip to content

Lemmas for `seq` and `seqZ` are inconsistent

Lemma fmap_seq j n : S <$> seq j n = seq (S j) n.
Lemma seqZ_fmap m m' n: Z.add m <$> seqZ m' n = seqZ (m + m') n.

Both in terms of naming, and their statements.