Simplification machinery for RA operations

One repeating point of frustration and confusion for new people learning Iris is how to deal with validity, composition, inclusion and updates of RAs that are composed by layering our combinators. Basically you need to peel off these combinators layer-by-layer and find the right lemmas each time, which can be very tricky, and even for an experienced Iris user this frequently takes way more time than it should. Things get worse because Coq's unification is often not able to apply these lemmas.

So @simonspies and @lepigre suggested we should have some (typeclass-based?) simplification machinery for these operations. Something that is able to e.g. turn ✓ (● Excl' n ⋅ ◯ Excl' m) into n = m, or {[l := x]} ≼ f <$> σ into exists y, σ !! l = Some y /\ f y ≼ x (and then if f = to_agree and x = to_agree v maybe even into σ !! l = v).