Zulip Chat Archive

Stream: maths

Topic: int.lt_succ_iff_le


view this post on Zulip 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...

view this post on Zulip Chris Hughes (Sep 23 2019 at 08:00):

Is it called int.lt_add_one?

view this post on Zulip Johan Commelin (Sep 23 2019 at 08:00):

Aah, nice lt_add_one_iff

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Sep 23 2019 at 08:03):

Really? Ugh, I should fix that.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 23 2019 at 08:04):

Aha, I see

view this post on Zulip Scott Morrison (Sep 23 2019 at 08:04):

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

view this post on Zulip Johan Commelin (Sep 23 2019 at 08:04):

Maybe it can try symmetry before applying...?

view this post on Zulip Johan Commelin (Sep 23 2019 at 08:04):

But maybe it costs too much

view this post on Zulip 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