chore(library/init/data): constructive nat

[Jack-Pumpkinhead]

Add lemmas to avoid classical.choice used in theorems/lemmas/defs prefix with nat.
(There are 121 usages, for example nat.strong_induction_on, nat.mod_lt, etc.

[digama0]

Rather than having nat versions of these theorems, I suggest importing the decidable.* order lemmas in algebra.order from mathlib and using them instead.

[digama0]

Also, it would be nice if this extended to int as well. Again, it should be as simple as applying the decidable.* theorems instead of the regular ones when constructing the instance.

[Jack-Pumpkinhead]

Oh.. int.decidable_le use (implicit) subtraction int.has_sub which comes from int.comm_ring which contains classical...

In other situations decidable.* is a good choice.

[digama0]

Right, because the proof of int.comm_ring uses facts about linear ordered rings (on nat, I think) that ultimately trace back to those theorems. I originally wrote the decidable.* series with exactly this refactor in mind, but that was before we unfroze the lean repo.