Also, refactor the file so that all type class + canonical structure instances
are at the same place, instead of spread through the file.

Move definitions and lemmas about heap_lang locations to module `Loc`

See merge request iris/iris!890

Improve iCombine to allow a 'gives' clause for validity properties

Closes #460

See merge request iris/iris!872

Rename `f_contractive_core` into `dist_later_intro`.

See merge request iris/iris!896

Change definition of dist_later for compatability with Transfinite Iris

See merge request iris/iris!886

Prove that invariants are "except 0".

See merge request iris/iris!897

In logatom lock: Formalize that the lock is Free before acquire.

See merge request iris/iris!891

Adapt to https://github.com/coq/coq/pull/16788

See merge request iris/iris!893

add big_opM_gset_to_gmap

See merge request iris/iris!878

add RA for integers with addition

See merge request iris/iris!879

Stronger version of `gmap_core_id`.

See merge request iris/iris!892

Extract dfrac notations

See merge request iris/iris!756

This fixes the fixme introduced in !554.
Coq issue #13654 was fixed by coq pr #14183.

Introduce bi_nsteps and add timeless results for bi closures

See merge request iris/iris!885