also use □ in bi_{least,greates}_fixpoint

See merge request iris/iris!716

persistent_fractional: strengthen like bi.persistent_sep_dup

See merge request iris/iris!717

In 13c5c1ad I strengthened bi.persistent_sep_dup
to support propositions that are persistent and either affine or absorbing; do
the same for `persistent_fractional`.

State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.

See merge request iris/iris!714

add big_sepS_{insert,delete}_2

See merge request !709

explain our choice of integer division operator

See merge request iris/iris!708

Modes for Equiv

See merge request iris/iris!701

Include workaround for Coq bug #14441, and drop now-failing test for that Coq
bug.

Fix typos

See merge request !706

register make_laterable as modality

See merge request iris/iris!636