upstream some list_numbers lemmas from Perennial

Also rename seq_S_end_app to seq_S_snoc, which I think better matches our usual name for lemmas involving _ ++ [_].

The proofs are by @tchajed.

added 2 commits

• 59b248ed - adjust variable names and remove redundant scope
• 794ce99a - add seqZ_S

Compare with previous version

I also added seqZ_S, which mirrors seq_S. Using S with a function taking Z might seem strange, but this does come up in a proof in Perennial.

added 1 commit

• c111795c - simplify proof (by Robbert)

Compare with previous version

resolved all threads

Also rename seq_S_end_app to seq_S_snoc

+1

Modulo comments this looks good. Please add a CHANGELOG entry :)

resolved all threads

added 2 commits

• c57fe844 - simplify proofs (by Robbert)
• d80a55ce - add changelog entry

Compare with previous version

Resolved all comments and added changelog entry.

merged

mentioned in commit 523920d1

Thanks!

mentioned in merge request !212 (merged)