| changeset 45933 | ee70da42e08a |
| parent 45931 | 99cf6e470816 |
| child 45965 | 2af982715e5c |
--- a/src/HOL/Nat.thy Mon Dec 19 14:41:08 2011 +0100 +++ b/src/HOL/Nat.thy Mon Dec 19 14:41:08 2011 +0100 @@ -1615,6 +1615,9 @@ lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)" by arith +lemma Suc_diff_Suc: "n < m \<Longrightarrow> Suc (m - Suc n) = m - n" +by simp + text{*Lemmas for ex/Factorization*} lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"