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.