improve `Rstruct.v`

[affeldt-aist]

It turns out that Rstruct.v was useful in PR #1002 and is also useful in porting results from infotheo (https://github.com/affeldt-aist/infotheo) to MathComp-Analysis but the file has not been maintained as well as other files. Improvements are welcome.

[affeldt-aist]

We have been using more extensively Rstruct.v for infotheo.0.6.0.
In particular, @t6s realized that we can now use the following, easier lemmas about Rinv and Rdiv: https://github.com/affeldt-aist/infotheo/blob/master/lib/ssrR.v#L642C1-L652C37
This can already be PRed as an improvement.
More generally, we should maybe reflect a bit on what we did with infotheo to PR a bit more improvements.
For example, real_realType is a bit longish for an identifier.
A multirule such as https://github.com/affeldt-aist/infotheo/blob/master/lib/ssrR.v#L657
might also be an improvement.
Should the lemmas about bigop also be part of the PR?
Mayve sumRE should not even exist but I am less sure about bigmaxRE.

[affeldt-aist]

Note that this (now merged PR) already introduced a few improvements: #1235