Cleanup Nat Lemmas

Stream: std4

[François G. Dorais]

std4#182 contains only cleaning and golfing edits to Nat.Lemmas. No breaking changes. It's ready to merge.

After that's done, I can breakup std4#177 into small chunks linked with Mathlib PRs to remove deprecated theorems.

[Notification Bot]

A message was moved here from #std4 > PR backlog by François G. Dorais.

[François G. Dorais]

(Split from #std4 > PR backlog: This thread is about bringing Std.Data.Nat.Lemmas up to standards.)

[François G. Dorais]

Some progress...

• std4#193 adds some handy custom recursors for Nat.
• std4#194 adds some new order lemmas and organizes old ones
• std4#195 adds some new succ/pred lemmas and organizes old ones
• std4#196 adds some new min/max lemmas (depends on std4#193)
• std4#197 adds some new add lemmas and tunes old ones
• std4#198 adds some new mul lemmas and deprecates some obscure ones
• std4#199 adds some new pow lemmas (depends on std4#193 and std4#198)
• std4#203 adds some new sub lemmas and cleans up old ones

[François G. Dorais]

That's a lot! I'm removing dependencies on std4#182 to make all of these more localized. I'm also generating Mathlib patches for each one.

[François G. Dorais]

Done! All of these are now independent of std4#182 and they all have working Mathlib patches!