refactor(data/real/nnreal): use `has_ordered_sub` (#9167)
* provide a `has_ordered_sub` instance for `nnreal`;
* drop most lemmas about subtraction in favor of lemmas from `algebra/ordered_sub`;
* add `mul_sub'` and `sub_mul'`;
* generalize some lemmas about `has_ordered_sub` to `has_add`;
* add `add_hom.mul_left` and `add_hom.mul_right`.
