| changeset 47208 | 9a91b163bb71 |
| parent 47108 | 2a1953f0d20d |
| child 47255 | 30a1692557b0 |
--- a/src/HOL/Nat.thy Fri Mar 30 08:10:28 2012 +0200 +++ b/src/HOL/Nat.thy Fri Mar 30 08:11:52 2012 +0200 @@ -252,6 +252,12 @@ apply (simp add:o_def) done +lemma Suc_eq_plus1: "Suc n = n + 1" + unfolding One_nat_def by simp + +lemma Suc_eq_plus1_left: "Suc n = 1 + n" + unfolding One_nat_def by simp + subsubsection {* Difference *}