# 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.