Make authoritative part of auth fractional

This follows #42 (closed). Somewhat related is #114 (closed).

This replaces Auth's carrier from Ex(M) to Frac * Ag(M). There are now 3 types of elements: ●{q} a, ◯ b, and ● a ≡ ●{1} a.

Cons: due to using Ag, Auth is not complete anymore, and does not enjoy Leibniz equality.

I tried to maintain the same interface of auth, and so far only lemmas concerning valid change interfaces. Changes to keep Iris built is very small (build tested locally with master at 8.9).

What do you think? @jung @robbertkrebbers @jjourdan @janno