feat(algebra/ordered_ring): add lemma (#6031)
feat(algebra/ordered_ring): add lemma (#6031)

Add a lemma in algebra.ordered_ring proving the inequality `a + (2 + b) ≤ a * (2 + b)`.

This is again part of the Liouville PR.





leanprover-community/mathlib,leanprover-community/mathlib