https://github.com/math-comp/math-comp.github.io/blob/0c5889105ecdf34bae9cb7d994ff4350c711d758/installation.org?plain=1#L36 "At some point, we should recommend rocq-mathcomp, since coq-mathcomp is just a compat metapackage." @proux01