feat: add set algebra support

[Kaptch]

Description

Adds set and finite sets interfaces to Std, set algebra and bigOpS. There's an example of usage in Examples/Namesets. Set algebra should work for LawfulSet (not necessarily finite) with decidable disjointedness.

This is still wip.
Before it can be finished, I will do two things:

• Double-check that all necessary lemmas are ported/add comments that link definitions/lemmas to Rocq names;
• Refactor some proofs to match the conventions.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[markusdemedeiros]

Hey! Great work on this PR, it's a very nice solution.

I left a lot of refactoring comments, many of them apply multiple times. If you want, I can do a cleanup pass on this PR, but I figured I'd give them to you first if you wanted to try. Let me know what you want to do.

[Kaptch]

Hi! Thank you for the review!
I made a few passes, keeping your comments in mind.
There's one place, where i thought that conv improves readability, but if there's strict no-conv policy, i don't mind changing it.

[markusdemedeiros]

Thanks for the updates, I'll do my best to give it another look soon!