Quentin VERMANDE

Great ! I could not test the first workaround (due to a lack of knowledge on my part), but the other two do work. Thank you very much.

The bench looks very good. [benchalgebra.ods](https://github.com/user-attachments/files/16440384/benchalgebra.ods)

This PR changes the behavior of `rewrite` and I do not understand why since I did not change the way the statements are declared.

After some investigation, that would be because I generalize some operations. Rewriting an equality about such an operation makes a coercion appear and subsequent rewrites see a composition of coercions...

`algebra_tactics` has to be generalized, since `add` is now on `addMagmaType` and not on `nmodType` anymore and the changes in `apery` depend on those in `algebra_tactics`, so I guess this...

Thanks for volunteering. I do not really have a constraint. It would be nice for it to be merged somewhat soon, because there are a lot of things I want...

I rebenched, and now have a 17% slowdown. [benchAlgebra.ods](https://github.com/user-attachments/files/16784429/benchAlgebra.ods)

> My understanding of the roles of `monoid.v` and `comoid.v` is that they respectively provide the multiplicative and additive hierarchies. Then, these two files seem to lack the symmetry: `comoid.v`...

Ah yes, I finally decided to postpone putting instances on dependent functions, because https://github.com/coq/coq/pull/19822 only solves some of the issues and it may be arbitrarily hard to make https://github.com/coq/coq/pull/19833 work....

The failure in analysis will be fixed by https://github.com/coq/coq/pull/19954 (this is actually the only instance I know of the issue). The one in mathcomp-reals I do not understand. With the...