feat(data/seq/seq): prove `seq.ext` earlier (#15830)
We heavily golf `seq.ext` and move it to almost the beginning of the file. Doing this breaks the proof of `seq.of_list_cons`, which we also change and golf by adding a few trivial `simp` lemmas (not all of them are needed, but might as well add them).
