Implement greatest fixed point inside the logic
In the interest of moving FP/iris-atomic!5 (closed) forward. Doing this inside the logic is good enough, and it is more conservative that going outside of the logic for this.
Implementation is by Robbert FP/iris-atomic!5 (comment 19496).