Should equality proofs in elementary-number-theory be abstracted?

[fredrik-bakke]

Since the carrier types are sets the proofs are already irrelevant so it seems reasonable to do this. On the other hand, the performance of the module is not currently a problem.