# HG changeset patch
# User paulson
# Date 1254411799 -3600
# Node ID b13e04329012662c70ab50ccfadf72e5bafc0163
# Parent  99843bbfaeb2283e40c7c614dcfb0ab173842942# Parent  45fa9254ddc815261615c1ffb096582806234e18
merged

diff -r 99843bbfaeb2 -r b13e04329012 src/HOL/Library/Nat_Int_Bij.thy
--- a/src/HOL/Library/Nat_Int_Bij.thy	Thu Oct 01 15:54:55 2009 +0200
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Thu Oct 01 16:43:19 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>"} *}