Merged requested to merge ralf/auth_frac_op into master
They were the only
_frac_ lemmas for these libraries, everything else is written as
_dfrac_ lemmas are general enough to cover the
frac case, so no reason to have these 3 specific lemmas (and not the dozens of others, corresponding to the dozens of other
_dfrac_ lemmas) -- it is more consistent to just remove these few outliers.
The only user of these lemmas that I found is GPFSL, and just using the
_dfrac_ lemma instead works fine there.