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.