# HG changeset patch
# User paulson
# Date 1254411773 -3600
# Node ID 45fa9254ddc815261615c1ffb096582806234e18
# Parent  02f412281b99f03f8372473919f16832522780de
Proved a new theorem: nat_to_nat2_inj

diff -r 02f412281b99 -r 45fa9254ddc8 src/HOL/Library/Nat_Int_Bij.thy
--- 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>"} *}