Fix typo in CHANGELOG

See merge request iris/stdpp!135

Rename performed in !131 was on drop_insert, not drop_length

random collection of lemmas

See merge request iris/stdpp!131

Remove trailing whitespace

See merge request !133

This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.

Replace explicit use of Inj instances by inj

See merge request !132

This was inconsistent and not explained before.

Update CHANGELOG for 1.3 release.

See merge request iris/stdpp!127

Fix both an error by my, and a provide compatibility with older Coq versions
whose `lia` is less powerful.

Make lemmas for `seq` and `seqZ` consistent.

Closes #57

See merge request iris/stdpp!126

Robbert/lookup total lemmas

Closes #50

See merge request iris/stdpp!125

For other operations, like `<$>`,  such lemmas appear to make little sense, since
they require premises involving `!!`.

Remove copyright headers, update LICENCE file.

Closes #54

See merge request !124

This follows iris!387
This closes issue #54.

Change mode of `TCEq`.

See merge request iris/stdpp!123

Set `Hint Mode` for logical `TCX` type classes

Closes #55

See merge request iris/stdpp!121

Avoid using Hint Resolve with a term

See merge request !122

This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.

Rename `fin_of_nat` → `nat_to_fin` to follow the conventions.

See merge request !120