Definition. num_lt_equi
num_lt X Y ↔ num_le X Y ∧ ¬∃f. sur f X Y