Make auth_update_core_id work with fractional authority
This MR does the following:
- Adds a new lemma
auth_update_core_idto 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_idand it doesn't seem useful for anything else.
- Instead of changing
auth_update_core_idone could instead have added a new lemma. That would be consistent with
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_idcontains 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