equal of le and not lt

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere more public than docs#linarith.eq_of_not_lt_of_not_gt? Is it true more generally?

example (a b : ℕ) (h : a ≤ b) (hb : ¬a < b) : a = b :=
linarith.eq_of_not_lt_of_not_gt _ _ hb h.not_lt

[Anne Baanen]

This should hold in any partial_order by contraposition of lt_of_le_of_ne, right?

[Anne Baanen]

That is:

example {α : Type*} (a b : α) [partial_order α] (h : a ≤ b) (hb : ¬a < b) : a = b :=
not_not.mp (mt h.lt_of_ne hb)

[Eric Wieser]

Do you think we should have eq_of_le_of_not_lt for convenience?

[Anne Baanen]

Sure, maybe calling it has_le.le.eq_of_not_lt for dot notation?

[Yury G. Kudryashov]

You can also do hle.eq_or_lt.resolve_right hlt.

[Yaël Dillies]

I find myself needing it as well so #10676 adds it to order.basic