The trick of using `Hint Constructors` was found in
`ZornsLemma.EnsemblesImplicit` which adds the same hint to the HintDb
`sets`.

Also, declare `Schutte_basics.ordinal` as a notation instead of as a
definition.

The file theories/ordinals/Schutte/Countable.v provides some theory
about countable `Ensemble`. The coq-zorns-lemma package contains very
similar results already.
This commit tries to use as many results from coq-zorns-lemma as
possible, instead of defining them in here.
Initial discussion on Zulip:
https://coq.zulipchat.com/#narrow/stream/344515-Hydras-.26-Co.2E-universe/topic/Library.20for.20countability.3F/near/341893039

This commit still contains some rough edges:
- The lemma `countable_singleton` could be incorporated in
  coq-zorns-lemma, instead of introducing it here.
- In some files we have to use `CountableTypes.foo` instead of mentioning
  the lemma `foo` directly, because adding `From ZornsLemma Require
  Import CountableTypes` messes up the scopes. This should be seen as a
  bug in `ZornsLemma`.