num_le_intro

Theorem. num_le_intro
(∃f. inj f X Y) → num_le X Y

Proof
num_le_intro. ⊢ (∃f. inj f X Y) → num_le X Y,
  bij_elimr num_le_equi.