## Stream: maths

### Topic: int.lt_succ_iff_le

#### Johan Commelin (Sep 23 2019 at 07:59):

lemma int.lt_succ_iff_le {m n : ℤ} :
m < n + 1 ↔ m ≤ n :=


This doesn't seem to be in mathlib. split; intro; linarith proves it but slowly...

#### Chris Hughes (Sep 23 2019 at 08:00):

Is it called int.lt_add_one?

#### Johan Commelin (Sep 23 2019 at 08:00):

Aah, nice lt_add_one_iff

#### Johan Commelin (Sep 23 2019 at 08:01):

I first had the sides swapped, and then library_search didn't find it. I thought you fixed that @Scott Morrison didn't you?

#### Johan Commelin (Sep 23 2019 at 08:03):

lemma int.lt_succ_iff_le {m n : ℤ} :
m < n + 1 ↔ m ≤ n :=
begin
symmetry,
library_search
end


#### Scott Morrison (Sep 23 2019 at 08:03):

Really? Ugh, I should fix that.

#### Scott Morrison (Sep 23 2019 at 08:04):

ohh... I see, yeah, library search can't do that out of the box. If you split; library_search it should succeed, however.

Aha, I see

#### Scott Morrison (Sep 23 2019 at 08:04):

It's a slight hack to do this, but I can add it.

#### Johan Commelin (Sep 23 2019 at 08:04):

Maybe it can try symmetry before applying...?

#### Johan Commelin (Sep 23 2019 at 08:04):

But maybe it costs too much

#### Keeley Hoek (Sep 23 2019 at 10:26):

I mean, symmetry probably costs exactly one more library_search_core invocation?

Last updated: May 19 2021 at 00:40 UTC