Skip to content

remove auth_frac_op lemmas

Ralf Jung requested to merge ralf/auth_frac_op into master

They were the only _frac_ lemmas for these libraries, everything else is written as _dfrac_. The _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.

Merge request reports