Theorem num_lt_intro

Proof
01. 1 ⊢ num_le X Y, hypo.
02. 2 ⊢ ¬∃f. sur f X Y, hypo.
03. 1, 2 ⊢ num_le X Y ∧ ¬∃f. sur f X Y, conj_intro 1 2.
04. 1, 2 ⊢ num_lt X Y, rsubj_elim num_lt_equi 3.
num_lt_intro. ⊢ num_le X Y → (¬∃f. sur f X Y) → num_lt X Y,
  subj_intro_ii 4.