Did anyone connect coq-prime to mathcomp. E.g. https://math-comp.github.io/htmldoc/mathcomp.ssreflect.prime.html

@Laurent Théry @Cyril Cohen ?

not that I know of. But do you need more than proving that prime mathcomp = prime in Z?

Thanks. That might indeed be sufficient for us. We'll see how how far it brings us.

Last updated: Jan 29 2023 at 18:03 UTC