# HG changeset patch
# User paulson
# Date 1079343961 -3600
# Node ID bbfa6b01a55f4e6002611a927fdf6c59b0562252
# Parent  b737e523fc6c5c1b209043641bea3ef4cdfb0d5c
new lemma

diff -r b737e523fc6c -r bbfa6b01a55f src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Mon Mar 15 10:45:31 2004 +0100
+++ b/src/HOL/Integ/NatBin.thy	Mon Mar 15 10:46:01 2004 +0100
@@ -353,6 +353,9 @@
 lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
 by (simp add: numerals)
 
+lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
+by (simp add: numerals)
+
 (* These two can be useful when m = number_of... *)
 
 lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
@@ -753,6 +756,7 @@
 val Suc_pred' = thm"Suc_pred'";
 val expand_Suc = thm"expand_Suc";
 val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
+val Suc_eq_add_numeral_1_left = thm"Suc_eq_add_numeral_1_left";
 val add_eq_if = thm"add_eq_if";
 val mult_eq_if = thm"mult_eq_if";
 val power_eq_if = thm"power_eq_if";