Add Fractional instance for AsFractional

AsFractional admits a very obvious Fractional instance in the case where it's of the form AsFractional (Φ q) Φ q. This commit defines that instance, which would help simplify proofs in #923.

Search issue

This loops with as_fractional_fractional in cases where the typeclass search can't progress in any better way. I've tried to figure out how to prevent it, and the most obvious way would be to remove the typeclass coercion on as_fractional_fractional.

I think doing so makes sense: the only case where the user would want this kind of coercion (and indeed the only place in the Iris codebase where it is used, AFAIK), is when there's an AsFractional in the environment and the user doesn't want to manually destruct it to apply the Fractional inside. I wouldn't expect to go from a Fractional goal backwards to an AsFractional with some evars, for example - but maybe this search behaviour is secretly necessary somewhere?

I would expect that the above case can somehow be handled with a less aggressive hint that doesn't allow for evars, but I couldn't figure out how to define it.