feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)
## Historical background
This tackles a problem that we have had for six years (#2697 for its move to mathlib, before it was in core): `ordered_semiring` assumes that addition and multiplication are strictly monotone.
This led to weirdness within the algebraic order hierarchy:
* `ennreal`/`ereal`/`enat` needed custom lemmas (`∞ + 0 = ∞ = ∞ + 1`, `1 * ∞ = ∞ = 2 * ∞`).
* A `canonically_ordered_comm_semiring` was not an `ordered_comm_semiring`!
## What this PR does
This PR solves the problem minimally by renaming `ordered_(comm_)semiring` to `strict_ordered_(comm_)semiring` and adding a new class `ordered_(comm_)semiring` that doesn't assume strict monotonicity of addition and multiplication but only monotonicity:
```
class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_le_mul_of_nonneg_left : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b)
(mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c)
class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α
class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b)
class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α
class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α :=
(zero_le_one : (0 : α) ≤ 1)
(mul_lt_mul_of_pos_left : ∀ a b c : α, a < b → 0 < c → c * a < c * b)
(mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α
class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b)
class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α
```
## Whatever happened to the `decidable` lemmas?
Scrolling through the diff, you will see that only one lemma in the `decidable` namespace out of many survives this PR. Those lemmas were originally meant to avoid using choice in the proof of `nat` and `int` lemmas.
The need for decidability originated from the proofs of `mul_le_mul_of_nonneg_left`/`mul_le_mul_of_nonneg_right`.
```
protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)]
(h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b :=
begin
by_cases ba : b ≤ a, { simp [ba.antisymm h₁] },
by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] },
exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le,
end
```
Now that these are fields to `ordered_semiring`, they are already choice-free. Instead, choice is now used in showing that an `ordered_cancel_semiring` is an `ordered_semiring`.
```
@[priority 100] -- see Note [lower instance priority]
instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α :=
{ mul_le_mul_of_nonneg_left := λ a b c hab hc, begin
obtain rfl | hab := hab.eq_or_lt,
{ refl },
obtain rfl | hc := hc.eq_or_lt,
{ simp },
{ exact (mul_lt_mul_of_pos_left hab hc).le }
end,
mul_le_mul_of_nonneg_right := λ a b c hab hc, begin
obtain rfl | hab := hab.eq_or_lt,
{ refl },
obtain rfl | hc := hc.eq_or_lt,
{ simp },
{ exact (mul_lt_mul_of_pos_right hab hc).le }
end,
..‹ordered_cancel_semiring α› }
```
It seems unreasonable to make that instance depend on `@decidable_rel α (≤)` even though it's only needed for the proofs.
## Other changes
To have some lemmas in the generality of the new `ordered_semiring`, I needed a few new lemmas:
* `bit0_mono`
* `bit0_strict_mono`
It was also simpler to golf `analysis.special_functions.stirling` using `positivity` rather than fixing it so I introduce the following (simple) `positivity` extensions:
* `positivity_succ`
* `positivity_factorial`
* `positivity_asc_factorial`
mathlib
f5a600f8 - feat(algebra/order/ring): Non-cancellative ordered semirings (#16172)
