refactor(*): more choice-free proofs (#7455)
Now that lean v3.30 has landed (and specifically leanprover-community/lean#560), we can finally make some progress on making a significant fraction of mathlib foundations choice-free. This PR does the following:
* No existing theorem statements have changed (except `linear_nonneg_ring` as noted below).
* A number of new theorems have been added to the `decidable` namespace, proving choice-free versions of lemmas under the assumption that something is decidable. These are primarily concentrated in partial orders and ordered rings, because total orders are already decidable, but there are some interesting lemmas about partial orders that require decidability of `le`.
* `linear_nonneg_ring` was changed to include decidability of `nonneg`, for consistency with linear ordered rings. No one is using this anyway so there shouldn't be any fallout.
* A lot of the `ordered_semiring` lemmas need `decidable` versions now because one of the core axioms, `mul_le_mul_of_nonneg_left`, is derived by LEM from an equivalent statement about lt instead of being an actual axiom. If this is refactored, these theorems can be removed again.
* The main files which were scoured of choicy proofs are: `algebra.ordered_group`, `algebra.ordered_ring`, `data.nat.basic`, `data.int.basic`, `data.list.basic`, and `computability.halting`.
* The end goal of this was to prove `computable_pred.halting_problem` without assuming choice, finally validating a claim I made more than two years ago in my [paper](https://arxiv.org/abs/1810.08380) on the formalization.
I have not yet investigated a linter for making sure that these proofs stay choice-free; this can be done in a follow-up PR.
