Equality proofs and proofs of propositions in elementary-number-theory should be abstracted

[fredrik-bakke]

Discussed in #1102

^{Originally posted by fredrik-bakke March 30, 2024}
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.

Note: This should be done as an isolated pull request. There may be some very exceptional instances where we do not want to abstract the proof because it, for instance, is particularly simple and has nice computational behavior, and that is okay.