[Merged by Bors] - feat(data/nnreal): filling out some lemmas

[semorrison]

From LTE.

---

[jcommelin]

I think all of these should also work for a linear_ordered_comm_group_with_zero. So that in the future they will also cover nnrat.
But I'm fine with merging this, and then we do a big generalization pass in the end, when Damiano's refactor is complete.

[adomani]

Dear Both,

I agree: these lemmas should be provable with more general assumptions. I might have just fixed the linarith issue with it, which means that I would be at the point where more of the group stuff has weaker hypotheses. The semiring/group_with_zero will be after that: there there is the further issue that multiplication is monotone only on the non-negative/positive elements, something that the current typeclasses are probably able to handle, but have not been tested yet.

The conclusion: I am happy to get this merged. After the refactor, it will be a festival of removing assumptions everywhere: I am only doing it in the most obvious places, with the most obvious weakenings.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests