[wip] port to HB

[gares]

It passes, there are mainly 3 problems:

• the FO step of rewrite kicks in is a different way, and a few rewrite have to be made more precise
• a perf problem with a hint extern declared in ssrnum
• HB.pack is uber slow in a few cases

[gares]

Help @CohenCyril for nix

[proux01]

Here is a rebased branch: https://github.com/proux01/odd-order/tree/hierarchy-builder

[gares]

you should be able to push to this branch now

[proux01]

Done (took me a while to figure out the name of the branch is hirarchy-builder without e 😢)

[gares]

surely a typo from me, sorry

[gares]

Thanks apparently it was not that hard, but I got tired and missed a /= and thought it was a deep problem.

[proux01]

Actually, the additional /= are less painful (except maybe when they require repeating a ! rewrite) than the (very few, only 5 instances here) associativity rewrite that require an additional pattern (but nothing specific to semirings here, we already experienced that with the HB port of mathcomp).