add subrange_of_matching_take lemma to seq_lib

[jonhnet]

Here's a lemma about Seq take and subrange I found valuable in verisplinter. I think it belongs in the seq library.

[jaybosamiya-ms]

I was surprised by the sudden introduction of the additional newline (after the comment) to satisfy the formatter in your second commit (94676cf). Turns out this was a subtle weirdness (triggered by comments immediately after an assert ... by { ... } or similar block that doesn't require a semicolon after it before the next statement) that was introduced likely when adding support for clauses/stanzas. This is now fixed in verus-lang/verusfmt#89 and should hopefully soon be part of the next verusfmt release (EDIT: Released in v0.4.2), and the unnecessary newline should no longer be required by the formatter (you will be allowed to keep it if you like, but you will no longer be forced to)