feat: Update later credits and fancy updates soundness proofs

[lzy0505]

Description

Fixes #396, following the recent MR in Rocq: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1217.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[Kaptch]

Thank you for the PR! I'll take a look in a moment

[Kaptch]

Nicely done! I added only minor fixes (mostly leftover isplit; iassumption in LaterCredits before we had iframe).
I think we can merge any time, but probably let's wait for Michael's comment about Hint Immediate.

While there shouldn't be problem anywhere with Plain->Persistent (at least, I don't remember any place, where it might be required, apart from soundness), it would be nice to know if there is a fix for it.

[markusdemedeiros]

Just briefly skimmed it, and it looks great :)

[lzy0505]

Thanks! Merging.