chore(computability/primrec): remove nolints

[vihdzp]

We add some documentation, and golf slightly by marking nat.elim and nat.cases as reducible.

---

[b-mehta]

I'm not sure if it's a good idea to mark new things as reducible, especially if the only benefit is some golf - sometimes reducible is regarded as code smell; so I'm very hesitant about this change being in a chore nolint PR.

[vihdzp]

No idea what I was thinking with the reducible tags, they've been reverted.

[riccardobrasca]

Thanks!

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests