Integration to mathcomp

[CohenCyril]

Hi @thery how about integrating your development to mathcomp?

[thery]

👍 but what about multinomial is it still in?

[palmskog]

@thery how about adding grobner.v to CoqEAL? This way, more people will be able to use it, since CoqEAL is part of the Coq Platform. CoqEAL already depends on Multinomials. Finally, the CoqEAL theory is already a form of incubator for results to add to regular MathComp.

[thery]

@palmskog Yep that was the plan a long time ago (beginning of the phD of Damien (Roughling)), I see if I can find some energy to properly do this

[thery]

@palmskog rocq-community/coqeal#70