Smaller changes:
- Reorders and reduces the imports in some files.
- In `_CoqProject`: re-enable the warnings about missing hint/instance
  localities
- Add hint/instance localities where they were missing. Use `#[export]`
  if possible.
- Changed some hint/instance localities to `#[export]`. This is a
  breaking change depending on the circumstances of the user code.

Having this definition will simplify the redefinition of homeomorphism.
Using `inverse_map` in the def. of homeomorphism will make the proofs
more conceptual (fewer hypotheses to juggle around), but this will need
a lot of changes.

It would make sense to use `inverse_map` in the definition of
`invertible`, but there's a lot that would need to be changed. That's
why I postpone doing so.

Rework definition of `homeomorphism`, `homeomorphic` and
`topological_property`. First, use `Definition` and `exists` instead of
`Inductive`. Second, for `topological_property` require the spaces to be
`homeomorphic` instead of requiring a `homeomorphism` between them (using the
`Proper` typeclass).
The former facilitates proving these properties and the latter facilitates
using proofs of `topological_property`, since in practice one rarely wants to
know the explicit homeomorphism between two spaces if one only wants to
transfer a topological property.

Then use the typeclass `Equivalence` to state that `homeomorphic` is an
equivalence relation. This will simplify proofs.

Use `inverse_map` throughout, instead of `bijective`. This makes it
easier to re-use lemmas.

Use `invertible` instead of `bijective` because it is a slightly
stronger property. In particular `FiniteT` behaves a bit better with
`invertible` than with `bijective`.

Move the definition of `eq_cardinal` from Cardinals to
FiniteTypes, because to do it the the other way around, some lemmas
would need to be moved.

Moves the definition of `eq_cardinal` to Cardinals, where it belongs.
But to allow this, the statements `countable_img_inj` and
`FiniteT_cardinality` had to be moved to Countable and FiniteTypes
respectively. In addition, `CountableT_cardinality` was removed, because
`CountableT` could be redefined in terms of `le_cardinal`, making the
lemma even more trivial.

Also, removes the file InfiniteTypes, because it has become empty.

The lemmas `Finite_as_lt_cardinal_ens` and
`injective_finite_inverse_image` currently are in `FiniteTypes.v`,
because their proofs use `FiniteT` in essential ways.

The files concerning cardinalities (`eq_cardinal` and `le_cardinal`) in
general are rather large and would be easier to manage if they are split
into multiple files.
This also solves a "practical" problem: the statement of `CSB` could be
formulated using `eq_cardinal`. But this is not possible if the file
`Cardinals.v` depends on the file `CSB.v`.
Another possibility would be, that `CSB` is carefully stated, that it
uses definitions compatible with `Cardinals.v`. But this would break
`Search`, or we'd need to re-state `CSB` in terms of `eq_cardinal` and
`le_cardinal` in `Cardinals.v`.

To make git happy, the file `ZornsLemma/Cardinals.v` is not included in
the previous commit. This way git can notice, that we moved
`ZornsLemma/Cardinals.v` to `ZornsLemma/Cardinals/Cardinals.v`. Thus
also `git blame` still works.
But the previous commit does not build.

Removed the `types_comparable` in favor of `le_cardinal_total`, because
both proved the same thing.

This moves everything deduced from `CSB` to `CSB.v`.

Also changes the statement of
`CountableT_is_FiniteT_or_countably_infinite` to be more fitting to the
rest of the theory.

The lemma says "unbounded subsets of ℕ are countably infinite", which
does not belong to the general discussion of cardinals.
It is a bit hard to sort this lemma into the existing files, but
CountableTypes.v seems to work best, because it already is concerned
with `nat`.

Also moves `Finite_as_lt_cardinal_ens` and
`injective_finite_inverse_image` to CountableTypes.v, because they
depend on `nat_unbounded_impl_countably_infinite`. This is not ideal.

A bit problematic is `nat_minimal_element_property_dec` and
`nat_minimal_element_property` which are not exactly proofs of
`Classical_Wf.minimal_element_property`. And they are self-contained,
not depending on any theory in CountableTypes.v.

These notions are redundant. If they are used in lemmas, they make
it harder to `Search` for results.

They hold independently of the def. `FiniteT` and are thus better placed
in the Cardinals folder.