Injective images of countable sets are countable

Add CI and claim of support for coq v8.17

Disables the requirement for hint locality. This needs to be done both
in `_CoqProject` and in the dune files.

Fix broken proof because of `d6d78d9`

Because `open_neighborhood` gets unfolded by `intuition`, the proof ends
earlier than the proof-script anticipated. This error was caused because
I didn't check whether the repo still compiles…

Add a hint for unfolding `open_neighborhood`

Fix the remaining `fragile-hint-constr` warning

Merge pull request #11 from coq-community/compatibility-fixes

Compatibility fixes

Fixing an import from ZornsLemma.

Addressing some warnings.

Adapting to Coq 8.8

Notation "'" was discontinued.

Adapting to Coq 8.7 representation of real constants.