Definition. lt_equi
a < b ↔ a ≤ b ∧ ¬a = b