Transfer of Bertrand's postulate to CoqPrime

[palmskog]

The first part of this project, the proof of Bertrand's postulate, is a generic result about primes, and could be useful to a larger audience. One way to accomplish this is to have the proof transferred into the CoqPrime project, which is in the Coq Platform and has regular releases compatible with the latest released version of Coq. However, this may require reorganization and adaptation to CoqPrime idioms.

After a tentative transfer, the project here could focus fully on providing verified programs that use Bertrand's postulate (on top of CoqPrime), both using the Why toolchain and using other means. Such programs and proofs are likely to have a much smaller audience, but are still very valuable to the community.