Improve the section on authoritative resource algebras

[jihgfee]

The section on authoritative resource algebras could benefit from a slight rewriting.
Some salient points:

• The generally presented rules for the RA are not sufficient for deriving the properties of the fractional use case
• There are some erratas, see below

Known erratas:

• The specifications of Exercise 8.52 do not recover the spatial isCounter predicate in the post-condition.
• Many definition use multiple ∀ x. ∀ y. ∀ z. _ rather than the iterated ∀ x, y, z. _
• The first RA construction uses m/n for the fragmental piece, but the generalised construction uses a/b