Proved a new theorem: nat_to_nat2_inj

--- a/src/HOL/Library/Nat_Int_Bij.thy	Thu Oct 01 15:19:49 2009 +0200
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Thu Oct 01 16:42:53 2009 +0100
@@ -128,6 +128,9 @@
   thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast
 qed
 
+lemma nat_to_nat2_inj: "inj nat_to_nat2"
+  by (simp add: nat_to_nat2_def surj_imp_inj_inv nat2_to_nat_surj) 
+
 
 subsection{*  A bijection between @{text "\<nat>"} and @{text "\<int>"} *}