[STATEMENT]
lemma Nset2finite_inj:"\<lbrakk>finite A; card A = Suc n; surj_to f {i. i \<le> n} A \<rbrakk> \<Longrightarrow>
        inj_on f {i. i \<le> n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; card A = Suc n; surj_to f {i. i \<le> n} A\<rbrakk> \<Longrightarrow> inj_on f {i. i \<le> n}
[PROOF STEP]
by (metis card_Collect_le_nat eq_card_imp_inj_on finite_Collect_le_nat surj_to_def)