author bulwahn Sat, 28 Jan 2012 10:22:46 +0100 changeset 46350 a49c89df7c92 parent 46349 b159ca4e268b child 46351 4a1f743c05b2
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
 src/HOL/Nat.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Nat.thy	Sat Jan 28 06:13:03 2012 +0100
+++ b/src/HOL/Nat.thy	Sat Jan 28 10:22:46 2012 +0100
@@ -1616,6 +1616,17 @@
lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
by simp

+(*The others are
+      i - j - k = i - (j + k),
+      k \<le> j ==> j - k + i = j + i - k,
+      k \<le> j ==> i + (j - k) = i + j - k *)
+
+text{*At present we prove no analogue of @{text not_less_Least} or @{text
+Least_Suc}, since there appears to be no need.*}
+
text{*Lemmas for ex/Factorization*}

lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
@@ -1669,17 +1680,6 @@
lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
using inc_induct[of 0 k P] by blast

-(*The others are
-      i - j - k = i - (j + k),
-      k \<le> j ==> j - k + i = j + i - k,
-      k \<le> j ==> i + (j - k) = i + j - k *)