bi/fixpoint lemmas

Follow-up to !718 (merged)

This MR upstreams a number of lemmas by @simonspies.

• least_fixpoint_ne' and 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_coind is the dual to least_fixpoint_strong_coind.
• greatest_fixpoint_paco offers 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.