split Zdivisibility from Znumtheory, deprecate most of Znumtheory

[andres-erbsen]

Repeat of approved PR rocq-prover/rocq#19789

Overlays (optional since addition of a compat Require):

• Require Znumtheory mit-plv/bedrock2#455
• Require Znumtheory mit-plv/fiat-crypto#2081
• Require Znumtheory before using it AbsInt/CompCert#548
• Require Znumtheory before using it math-comp/mczify#60
• https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/605

[proux01]

According to the last message on the original PR rocq-prover/rocq#19789 (comment) I was just waiting for you to open the PR here (I even did the rebase for you, you just had to click the provided link) and promised to review/merge it quickly. Alas, this was four months ago, I no longer have time for it right now.
So if no one else takes over, feel free to merge if you're happy with it, once CI is green (it seems pretty unhappy right now).

[andres-erbsen]

Note that this PR is not the straightforward rebase from january but rather a version adapted to work with the component-dependency-restricted build, including some changes to the component dependencies.

[andres-erbsen]

I added a compat require of Znumtheory in ZArith, split up the changelog by category, and changed deprecations to say 9.1.

I intend to merge if CI passes.