[Merged by Bors] - feat(algebra/ordered_monoid): inequalities involving mul/add

[benjamindavidson]

I couldn't find some statements about inequalities, so I'm adding them. I included all the useful variants I could think of.

[eric-wieser]

Pretty much all these lemmas take an h argument only to apply either le.trans or le.trans_lt on it with an existing proof. I'm not sure some_long_name h ... is really better than (some_short_name ...).trans h, and therefore whether these lemmas are worth having,

[benjamindavidson]

I think in cases like this it's always worth adding the exact statement, even if it's just so it will be generated by library_search (which makes things easier and more accessible for those less familiar with the repository). Moreover, by way of example,

example {a b c : ℝ} (h : a^2 + b^2 < c) : -sqrt c < a ∧ a < sqrt c :=
begin
  have : a^2 < c,
  { simpa only [add_zero] using (add_le_add_left (pow_two_nonneg b) (a^2)).trans_lt h },
  exact sqr_lt.mp this,
end

is significantly longer and more convoluted than

example {a b c : ℝ} (h : a^2 + b^2 < c) : -sqrt c < a ∧ a < sqrt c :=
sqr_lt.mp (lt_of_add_lt_left h (pow_two_nonneg b))

I also believe that @jcommelin is in favor of adding these lemmas -Johan, can you please confirm (or correct me if I'm wrong)?

[semorrison]

I think in cases like this it's always worth adding the exact statement, even if it's just so it will be generated by library_search (which makes things easier and more accessible for those less familiar with the repository). Moreover, by way of example,

I'm in favour of adding lemmas like these. I don't think their existence causes any harm, and easy inequalities have such a high Lean-effort : IRL-effort ratio that any help (e.g. library_search) is useful.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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