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