Definition. num_le_equi
num_le X Y ↔ ∃f. inj f X Y