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.