## Stream: Is there code for X?

#### Benjamin Davidson (Feb 11 2021 at 03:47):

Does the following exist in mathlib?

import analysis.special_functions.trigonometric

example (a b c : ℝ) (h : a + b < c) (hle : 0 ≤ b) : a < c := by linarith


As you can see, this can be proven easily by linarith, but I was surprised that I couldn't find an exact statement.

(The import is random)

#### Johan Commelin (Feb 11 2021 at 05:45):

How many variations are there on this lemma? I guess it makes sense to add these, but then we also need things like

example (a b c : ℝ) (h : a < b + c) (hle : b ≤ 0) : a < c := _


And also variants where h is a \le and hle becomes hlt.
I guess mathlib already has the variant where everything is \le, right?

#### Benjamin Davidson (Feb 11 2021 at 05:49):

For that matter, I can't find

example (a b c d : ℝ) (h : a + b < c) (hle : d ≤ b) : a + d < c := by linarith


either...surely this must exist in the library?

#### Benjamin Davidson (Feb 11 2021 at 05:51):

Johan Commelin said:

I guess mathlib already has the variant where everything is \le, right?

No, I couldn't find the le variant either.

#### Benjamin Davidson (Feb 11 2021 at 05:51):

Perhaps searching with ℝ is too specific?

#### Johan Commelin (Feb 11 2021 at 05:54):

Ooh, right, this is probably a statement about linearly ordered rings

#### Benjamin Davidson (Feb 11 2021 at 06:01):

I just tried a library_search with a, b, and c as members of a linearly ordered ring and got a deterministic timeout :(

#### Benjamin Davidson (Feb 11 2021 at 06:06):

I don't mind adding these but I'd be pretty surprised if none of the variants already exist.

#### Benjamin Davidson (Feb 11 2021 at 08:21):

#6171

Last updated: May 07 2021 at 21:10 UTC