bbN which `le_lt` or `lt_le` between adjacent bbNs

Stream: Is there code for X?

[Jihoon Hyun]

It seems like there is no lemma like below. If it really isn't present, I'd like to make a pr for adding these. Please tell me if these are too elementary to be added somewhere in the library.

theorem le_and_lt_succ {m n : ℕ} (h₁ : m ≤ n) (h₂ : n < m.succ) : n = m :=
  le_antisymm (lt_succ.mp h₂) h₁

theorem lt_and_le_succ {m n : ℕ} (h₁ : m < n) (h₂ : n ≤ m.succ) : n = m.succ :=
  le_antisymm h₂ h₁

Aside from that, can this be applied to IsWellOrdered as well?

[Yury G. Kudryashov]

Whether to add these two lemmas about Nat is a question to #std4 maintainer(s). AFAIR, @Mario Carneiro is one (of two? three?) of them.

[Yury G. Kudryashov]

A version for Order.succ would be a question for Mathlib.

[Yaël Dillies]

I think we should always normalise a < b.succ to a ≤ b and a.succ ≤ b to a < b, so I would be again the first one.

[Mario Carneiro]

The lemmas look fine to me, I've definitely felt the need for them in the past (it is a combination of two lemmas but it would still be nice to have just one). Not so sure about the names though, and should not be involved since there is no And in the statement

[Yury G. Kudryashov]

le_antisymm_lt_succ?

[Mario Carneiro]

that would make more sense with the antisymm at the end, no?

[Yaël Dillies]

eq_of_le_of_lt_succ is the Yaël-approved name.