# Make auth_update_core_id work with fractional authority

This MR does the following:

- Adds a new lemma
`to_agree_includedN`

- Generalizes
`auth_update_core_id`

to only require a fractional authority.

A few remarks/potential points of discussion:

- I've removed the lemma
`core_id_local_update`

. It can't be used to prove the generalized`auth_update_core_id`

and it doesn't seem useful for anything else. - Instead of changing
`auth_update_core_id`

one could instead have added a new lemma. That would be consistent with`auth_both_op`

and`auth_both_frac_op`

. But, to me it seems like such a simple generalization/specialization is not worth two lemmas. - The proof of
`auth_update_core_id`

contains a bit of duplication in the two branches. I was not able to cut down on it (my attempts only resulted in larger proofs), but maybe someone else can😄