Use dfrac everywhere
view support dfrac now, but many of the abstractions built on top of it do not yet:
There are more
auth-based abstractions in
algebra.lib but those do not expose any fraction on their authoritative part yet.
Some more are not actually built on top of
view, but these are or could be exposing fractions that it might be useful to turn into
Saved propositions (could be made essentially "
ghost_varwith higher-order ghost state", supporting both persistent immutable and ephemeral mutable saved propositions)
However, before we do all this, we should figure out if there is a way to do that without making these APIs harder to use for the common case of only needing fraction
gset_bij, we are already in the situation that users need to write
DfracOwn 1 a lot; I wouldn't want the same to happen e.g. for