n < nat.succ m ↔ n ≤ m

Stream: Is there code for X?

[Eric Wieser]

Do we really not have this?

lemma lt_succ_iff_le {n m : ℕ} : n < nat.succ m ↔ n ≤ m :=
⟨le_of_lt_succ, lt_succ_of_le⟩

library_search couldn't find it with import data.nat.basic, but maybe I missed an import. Neither docs#nat.lt_succ_iff_le or docs#nat.le_iff_lt_succ exist.

[Rémy Degenne]

docs#nat.lt_succ_iff

[Eric Wieser]

Thanks, I guess it was defined lower down in the file than where I was trying to prove it

[Anne Baanen]

By the way, n < m.succ is defeq to n.succ ≤ m.succ, so you can golf your proof to succ_le_succ_iff.

[Anne Baanen]

(Which is in fact what the source code does :P)

[Eric Wieser]

In #8224 I actually ungolfed the proof, because it makes it easier to find the one-directional lemmas

[Eric Wieser]

My workflow is quite often:

• Use the iff with an mp or mpr in my proof
• Go to definition
• Hope the proof is ⟨mp, mpr⟩ so I can use the more specific (and usually shorter) lemma