bump to 4.26

[alexanderlhicks]

A pain free bump to v4.26.0. This should help resolve the build issue in COmpPoly (Verified-zkEVM/CompPoly#4)

[dhsorens]

Nice and easy!

[Julek]

This is quite broken, it seems batteries has introduced a bunch of theorems with names clashing with theorems in this library, not all of them match the statements, so some non-trivial work needs to be done here. Doesn't compile.

[alexanderlhicks]

hmm interesting, it built fine locally 🤔

edit: nvm it does seem broken now, let me investigate.

[dhsorens]

Investigating this. Proofs are easy to fix, there's just the question of what to do with the conflicting theorem names. The theorems in batteries etc seem to be simpler than the ones in this library but I'm not 100% sure how compatible they are or whether they're a simple, generalized replacement to the ones here. Options include:

1. renaming the local clashing theorems with a _legacy or _temp suffix, or something with an aim to deprecate them
2. rename the clashing theorems to make them more descriptive of the way they differ from the new standard theorems, with no (short-term) aim to deprecate

@alexanderlhicks @Julek I think the way to go may be number 2, it keeps the lemmas we have. We should probably go thru Arklib and CompPoly and edit the proofs to use the new mathlib theorems, and if we stop using any here completely we can deprecate.

[dhsorens]

see new PR #5 for proposed changes. in CompPoly and Arklib the best thing to do is probably try to adopt the new standard theorems/lemmas, but with these new more descriptive names we can also keep these theorems locally without needing to deprecate