mathlib3

1b0e5ee5 - chore(data/real/nnreal): avoid abusing inequalities in nnreals (#7872)

chore(data/real/nnreal): avoid abusing inequalities in nnreals (#7872) I removed the use of `@`, so that all implicit arguments stay implicit. The main motivation is to reduce the diff in the bigger PR #7645: by only having the explicit arguments, the same proof works, without having to fiddle around with underscores.