src/HOL/Nat.thy
 changeset 46350 a49c89df7c92 parent 46028 9f113cdf3d66 child 46351 4a1f743c05b2
```     1.1 --- a/src/HOL/Nat.thy	Sat Jan 28 06:13:03 2012 +0100
1.2 +++ b/src/HOL/Nat.thy	Sat Jan 28 10:22:46 2012 +0100
1.3 @@ -1616,6 +1616,17 @@
1.4  lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n"
1.5  by simp
1.6
1.7 +(*The others are
1.8 +      i - j - k = i - (j + k),
1.9 +      k \<le> j ==> j - k + i = j + i - k,
1.10 +      k \<le> j ==> i + (j - k) = i + j - k *)
1.14 +
1.15 +text{*At present we prove no analogue of @{text not_less_Least} or @{text
1.16 +Least_Suc}, since there appears to be no need.*}
1.17 +
1.18  text{*Lemmas for ex/Factorization*}
1.19
1.20  lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
1.21 @@ -1669,17 +1680,6 @@
1.22  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
1.23    using inc_induct[of 0 k P] by blast
1.24
1.25 -(*The others are
1.26 -      i - j - k = i - (j + k),
1.27 -      k \<le> j ==> j - k + i = j + i - k,
1.28 -      k \<le> j ==> i + (j - k) = i + j - k *)