proposition: Lemma N_inj_le m n (f : N m -> N n) : injective f -> m <= n.
proof: Proof. intro f_inj. assert (e : length (map f (L m)) = m). rewrite map_length, length_L. refl. rewrite <- e, <- (@length_L n). apply nodup_incl_length_le. apply nodup_map_inj. hyp. apply nodup_L. intros y hy. destruct y as [y_val y]. apply In_L. Qed.
imports: CoLoR(LogicUtil NatUtil ListUtil ListNodup FunUtil VecUtil)