instantiate GRinv.inv directly by Rinv, deprecating Rinvx

[t6s]

Motivation for this change

In reals_stdlib/Rstruct.v, GRing.inv has been instantiated not by Rinv, but Rinvx,
which is separately defined in Rstruct but is extensionally equal to Rinv.
This PR removes this redundancy and deprecates Rinvx.

Infotheo will benefit from this change when extracting real-number algorithms.
(affeldt-aist/infotheo#142)

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels