Add primop backed versions of natural-number operations

[Taneb]

One possible solution for #1427

I add versions of min, max, and dist that use primitive operations so they compile to fast code (hopefully - I admit I haven't checked this yet). I also add proofs that they match their recursively defined counterparts, and a proof about distance that I felt was missing.

[MatthewDaggitt]

Sorry for taking so long to review this. Looks fine to me. Can you add a CHANGELOG entry?

[Taneb]

Sure, I'll add a changelog entry in the next few days