odd-order
odd-order copied to clipboard
math-comp
The formal proof of the Odd Order Theorem
Modifications corresponding to the PR https://github.com/math-comp/math-comp/pull/207
Some proofs rely on the fact that the proof of membership in I_n comes from inZp, which is not the case anymore with https://github.com/math-comp/math-comp/pull/1229.
I'm observing the issue that `rewrite (can_eq (dprod_IirrK _))` or just type-checking `can_eq (dprod_IirrK _)` is surprisingly slow in `PFsection4.v`. We need to investigate it.
There is a rewrite that triggers a higher order unification problem whose RHS changes due to https://github.com/coq/coq/pull/19987. The rewrite was not actually needed, so I bypassed it.
Adapt to https://github.com/math-comp/math-comp/pull/1354
