Add RA for auth of a heap

auth (gmap X Y) is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use gen_heap when really they want this RA, I am now convinced that we should have it in Iris. ;)

The only open question for me is, what is Y? (X is any countable type.)

• We probably should have fractions, so that would be Y := frac * agree T. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives False).
• @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with Y := agree T, or we could do the strictly more powerful thing (subsuming both of the above) and do Y := (frac * agree T) + agree T. I think with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.