Strengthen `bi_mono_pred` to ensure that functions are non-expansive.

Simuliris currently contains a copy of the bi.lib.fixpoint that contains the strengthened version.

Note: Simuliris contains a bunch of other lemmas about bi.lib.fixpoint, I leave those to @simonspies to upstream.