mulr_rev out of forms.v

[affeldt-aist]

Motivation for this change

fixes #1092

mulr_rev had nothing to do in derive.v

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md

~~- [] added corresponding documentation in the headers~~

Compatibility with MathComp 2.0

• [x] I added the label TODO: HB port to make sure someone ports this PR to the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

There is certainly something smarter to do with R^c.

[affeldt-aist]

@CohenCyril Since you thumbs uped the corresponding you may have an interest in this PR. Otherwise, we'll postpone to 1.0.0.

[CohenCyril]

@CohenCyril Since you thumbs uped the corresponding you may have an interest in this PR. Otherwise, we'll postpone to 1.0.0.

This should ultimately be backported to mathcomp, but there is no emergency here.

[affeldt-aist]

mulr_rev definition unfolded, as discussed during the last MathComp-Analysis dev meeting.

[affeldt-aist]

Ok, it looks like the HB.instance for the R^c case is of no use in MathComp-Analysis...

[proux01]

Let's remove it then. Just to be sure, is the revop structure used then?

[affeldt-aist]

I check and report asap.