port existing proofs to ssreflect 1.9.0

From the mathcomp 1.9.0 release notes:

> removed Coq prelude hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm, to
> improve robustness of by ...; scripts may need to invoke addn0,
> addnS, muln0 or mulnS explicitly where these hints were used
> accidentally.

=> This patch makes these required fixes in Prosa.

While at it, turn on CI for coq:dev and Coq 8.9 with two versions of ssreflect.
3 jobs for master in 3 minutes and 48 seconds (queued for 1 second)
Status Job ID Name Coverage
  Build
passed #33096
coq:8.9

00:03:48

passed #33095
coq:8.9+ssreflect:1.8.0

00:03:39

failed #33097
allowed to fail
coq:dev

00:01:03

 
Name Stage Failure
failed
coq:dev Build There is an unknown failure, please try again
File "./util/seqset.v", line 19, characters 42-52:
Error: The reference mkPredType was not found in the current environment.

Makefile:658: recipe for target 'util/seqset.vo' failed
make[1]: *** [util/seqset.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
Makefile:320: recipe for target 'all' failed
make: *** [all] Error 2
ERROR: Job failed: exit code 1