refactor(data/real/ennreal): remove sub lemmas (#9857)
* Remove all lemmas about subtraction on `ennreal` that are special cases of `has_ordered_sub` lemmas.
* [This](https://github.com/leanprover-community/mathlib/blob/fe5ddaf42c5d61ecc740e815d63ac38f5e94a2e8/src/data/real/ennreal.lean#L734-L795) gives a list of renamings.
* The lemmas that have a `@[simp]` attribute will be done in a separate PR
