# Commit 2021-09-15 18:42 8185637f

View on Github →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`

.