Coq 8.20 support

[palmskog]

For some reason, Coq 8.20.0 is not supported. Here's the error I got:

File "./src/selection.v", line 329, characters 5-53:
Error: The LHS of up_divS
(up_div _.+1 _)
does not match any subterm of the goal

If I had to guess, it may be related to how the semantics of SSReflect's have changed - it's now sort-polymorphic and opaque, and one may have to switch to have @H instead of have H in some places to get desired transparency.