a < b ∧ a = b → false

Stream: Is there code for X?

[Bernd Losert]

Is there a lemma like this somewhere for a partial order? I can't seem to find one. library_search didn't find one either.

[Anne Baanen]

You can do this using docs#has_lt.lt.ne:

import order.basic

example {α : Type*} {a b : α} [preorder α] (hlt : a < b) (heq : a = b) : false :=
hlt.ne heq

[Yaël Dillies]

or docs#eq.not_lt, for the flipped way

[Bernd Losert]

Cool. Thanks.