false_of_lt_of_lt

Stream: Is there code for X?

[Eric Wieser]

I'm surprised that linarith can't solve this:

import tactic.linarith
import order.complete_boolean_algebra

example {R} {a b : R} [linear_order R] (hab : a < b) (hba : b < a) : false :=
by linarith [hab, hba] -- fails

example {R} {a b : R} [linear_order R] (hab : a < b) (hba : b < a) : false :=
(hab.trans hba).not_le le_rfl -- ok

Do we have this as a lemma anywhere?

[Alex J. Best]

Linarith is linear arithmetic, but here there is no arithmetic, that is, linarith requires a linear ordered commutative ring https://leanprover-community.github.io/mathlib_docs/tactic/linarith/frontend.html

[Eric Wieser]

Ah indeed, linarith is happy to solve it with linear_ordered_comm_ring