Drop support for Coq 8.20

[proux01]

Maybe something we want to do after the next release (this will also enable improving the deprecations by using use=).

Cc @affeldt-aist

[affeldt-aist]

What about merging it now for the release of 1.16.0?
I am asking because

• there was a Coq 8.20 related CI problem in another PR Tail expectation formula for L1 random variable #1865 (comment) , I don't get the error and I am not able to reproduce it by recreating an opam environment with Coq 8.20 and MathComp 2.4.0
• Rocq 9.0 and Rocq.9.1 seem to be both supported, so we abide by the "at least two versions supported" rule

[proux01]

My reasoning was that if the current master supports 8.20 you may as well do a last release supporting it before dropping it. But if you want to fit #1865 in the release, then it may indded make sense to merge the current PR first. No strong opinion here, in any case the current PR is mergeable so do as you prefer.

[affeldt-aist]

Thanks for the information. Then unless somebody figures out a solution I think we'll merge before the release.