mathlib3

8a60fd75 - refactor(data/ennreal/basic): prove has_ordered_sub instance (#9582)

refactor(data/ennreal/basic): prove has_ordered_sub instance (#9582) * Give `has_sub` and `has_ordered_sub` instances on `with_top α`. * This gives a new subtraction on `ennreal`. The lemma `ennreal.sub_eq_Inf` proves that it is equal to the old value. * Simplify many proofs about `sub` on `ennreal` * Proofs that are instantiations of more general lemmas will be removed in a subsequent PR * Many lemmas that require `add_le_cancellable` in general are reformulated using `≠ ∞` * Lemmas are reordered, but no lemmas are renamed, removed, or have a different type. Some `@[simp]` tags are removed if a more general simp lemma applies. * Minor: generalize `preorder` to `has_le` in `has_ordered_sub` (not necessary for this PR, but useful in another (abandoned) branch).