Added [cmra_update_included] lemma

There is currently no way of weakening a fragment in the scope of the frame-preserving update of the authoritative RA (without breaking abstraction). It is thus proposed to add the rule:

Lemma auth_update_frag_included a b : b ≼ a → ◯ a ~~> ◯ b

One use of this is the instructive example of proving the following frame-preserving update for a simpler variant of the mono_nat RA:

(●MN n ⋅ ◯MN m) ~~> (●MN (n + x) ⋅ ◯MN (m + x))

In particular, this example follows from auth_update, max_nat_local_update, and auth_update_frag_included.

Note that the current version of mono_nat employs the pattern of keeping a copy of the persistent fragmental part within the authoritative abstraction, making this approach a bit less important.

I could however imagine other cases in which the lemma could be useful, although I fail to come up with them now.

EDIT:

Instead added the following lemma:

Lemma cmra_update_included x y : x ≼ y → y ~~> x

The originally intended lemma can be directly derived from this and have thus not been added, for consistency with remaining similar RA constructions.