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 😄