affeldt-aist

We should now remove it and use MathComp instead.

i have not yet done the changelog and I have not yet moved the lemmas to the right files but this might wait a first round of review I think...

This would require to also move `RevOp` out of `forms.v` to say `mathcomp_extra.v`, is that ok? @CohenCyril

I made a first pass. A few things (doc) were not moved, a few removed things were not documented in the changelog, and I formatted a bit the documentation and...

As a last check I mostly checked the doc for typos. It just needs a rebase before being merged I think.

I added two NBs and force-pushed to merge asap.

NB: partly addressed by PR #1166, now merged

> shouldn't this work depend on monae now? one thing is that monae is not yet ported to mathcomp-analysis 1.0.0, that makes it more difficult @t6s

NB: It goes through in this slightly different configuration: ```text # Packages matching: installed # Name # Installed # Synopsis atd 2.15.0 Parser for the ATD data format description language...

> Contains a patch of contra that we may want to extract. Do you mean that it ought to be a different PR? (That may help the review process.)