src/HOL/Nat.thy
changeset 30128 365ee7319b86
parent 30093 ecb557b021b2
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Nat.thy	Thu Feb 26 06:39:06 2009 -0800
     1.2 +++ b/src/HOL/Nat.thy	Thu Feb 26 08:44:12 2009 -0800
     1.3 @@ -701,6 +701,9 @@
     1.4  lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
     1.5  by (simp add: diff_Suc split: nat.split)
     1.6  
     1.7 +lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
     1.8 +unfolding One_nat_def by (rule Suc_pred)
     1.9 +
    1.10  lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
    1.11  by (induct k) simp_all
    1.12  
    1.13 @@ -1135,7 +1138,7 @@
    1.14    by (cases m) (auto intro: le_add1)
    1.15  
    1.16  text {* Lemma for @{text gcd} *}
    1.17 -lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
    1.18 +lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
    1.19    apply (drule sym)
    1.20    apply (rule disjCI)
    1.21    apply (rule nat_less_cases, erule_tac [2] _)