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.

added 17 commits

• 27b3ca52...8045a633 - 14 commits from branch RT-PROOFS:master
• 9b8d14ef - re-enable CI testing of the latest Coq and ssreflect versions
• d38e9112 - update CI to test Coq 8.9 + latest ssreflect
• 6740cbb8 - port existing proofs to ssreflect 1.9.0

Compare with previous version

merged