int.lt_succ_iff_le

Stream: maths

[Johan Commelin]

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]

Is it called int.lt_add_one?

[Johan Commelin]

Aah, nice lt_add_one_iff

[Johan Commelin]

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]

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

[Scott Morrison]

Really? Ugh, I should fix that.

[Scott Morrison]

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

[Johan Commelin]

Aha, I see

[Scott Morrison]

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

[Johan Commelin]

Maybe it can try symmetry before applying...?

[Johan Commelin]

But maybe it costs too much

[Keeley Hoek]

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