Merged requested to merge lgaeher/iris:fixpoint-lemmas into master
Follow-up to !718 (merged)
This MR upstreams a number of lemmas by @simonspies.
greatest_fixpoint_ne'are useful for stating non-expansiveness of the fixpoints in terms of the function the fixpoint is taken of. Currently, they are not instances as I'm unsure as to how useful they would be as instances.
greatest_fixpoint_strong_coindis the dual to
greatest_fixpoint_pacooffers a form of parameterized coinduction. We don't currently use this lemma in Simuliris due to the more complicated fixpoint construction, so I don't have a strong opinion on whether it should be upstreamed or not, but it still seems like a useful lemma to have.