I'd like to partition a sequence s with a predicate p, producing two sequences is_p and not_p. Post conditions would be that every element in p is now in is_p or not_p, in the appropriate order and nothing else is in them.
These seems like something that others would have already done. Is that likely? Is anyone building a library of useful Dafny code? Is there any way to search for such bits of Dafny code? Do people do GitHub code searches?
There is effort to build dafny library, see library. Particular function you are looking for is here