This is in preparation of a pull request to MathComp to push generic lemmas upstream (I only went through util/nat.v anf util/sum.v for now). Merge plan:
do a pull request on MathComp with the lemmas tagged TODO: PR MathComp
when this PR is merged, adapt the current merge request and change the TODO comments into something like "will be in MathComp 1.15"
merge the current merge request
once MathComp 1.15 (or 2.0) is released and becomes the minimal version in Prosa, remove the tagged lemmas
Is there a volunteer to open the upstream pull request? I could certainly do it but I don't feel the most legitimate, not being an actual Prosa author. Note that I probably already made most of the work here by rewriting the proofs in a more MathComp style, so the procces should be reasonnably light. It's also a great opportunity to learn more about MathComp and how to write short and robust proof scripts with ssreflect.
Björn Brandenburg authored
