Add proof of 45, The Partition Theorem

[ksk]

I wrote down a formal proof of the Euler's Partition Theorem.
The proof script requires mathcomp, hierarchy-builder, and zify.
I tested it on the following two combinations:

• coq 8.19.2, mathcomp 2.3.0, hierarchy-builder 1.8.0, zify 1.5.0
• rocq 9.0.0, mathcomp 2.4.0, hierarchy-builder 1.10.0, zify 1.5.0

both of which accept it.

[ksk]

@jmadiot
I want you to follow up on this PR. The CI checking fails just due to the CI environment being outdated rather than an issue with the script itself. Please let me know if there’s anything I can do to help address this or move the PR forward.

[jmadiot]

Hi, sorry for the long delay, and nice one!

Do you think you could host the proof script somewhere else, like a repository that we will reference, with also a README with instructions to install the dependencies (e.g. a sequence of opam commands)?

I would like to not add dependencies to this repository -- and maybe move proofs somewhere else eventually.