Port to ssreflect 1.9

The latest release of mathcomp breaks a couple of proofs in Prosa. This patch enables CI testing for ssreflect 1.9.0 and fixes the broken proofs. Unless there are any complaints, I'll merge this shortly.

Note @mlesourd @sophie @fradet @monin @xiaojie: this touches the TDMA WCRT proof (in a trivial way), so please integrate this fix when porting the analysis to the "new Prosa".

CC: @sbozhko

NB: Prosa is currently broken on the development version of Coq, too, but the required fix (like this one https://github.com/math-comp/finmap/commit/4cf617b5b0af8ed2b48360feb8a1e28a323cdbfe) breaks compatibility with mathcomp 1.8.0 on Coq 8.9, which I believe is still used by some. I'll file an issue to keep track of this. In the long run, it would be good if we could retire our own homegrown version of finite sets in favor of the forthcoming finmap library in mathcomp.