Modernising Data.Nat.Properties

[jamesmckinna]

Two quick thoughts, plus a placeholder:

• currently, there is no use of variables !
• suc-injective can be made lazier by redefining it as cong pred, and systematically replacing uses of that compound elsewhere?
• anything else?

NB this is intended to be cosmetic for v2.0, not the systematic overhaul envisaged by @JacquesCarette in #1925

Note to self: could be folded into any PR addressing #2087

[jamesmckinna]

I'm sure that this sort of issue will recur, but closing this now (and should have, after #2089).

[MatthewDaggitt]

@jamesmckinna when you close issues because a PR has addressed them, can you check that there's the correct Milestone added and the PR is linked against in the Development box (both on the RHS). Makes it a little easier to sort and filter historical issues when doing archaeology!

[jamesmckinna]

Certainly! Sorry to have missed your comment until now.