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:
TODO: PR MathComp
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.