src/HOL/Num.thy
changeset 47218 2b652cbadde1
parent 47216 4d0878d54ca5
child 47220 52426c62b5d0
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 11:16:35 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 11:52:26 2012 +0200
     1.3 @@ -919,6 +919,12 @@
     1.4  lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k"
     1.5    by (simp add: numeral_eq_Suc)
     1.6  
     1.7 +lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k"
     1.8 +  by (simp add: numeral_eq_Suc)
     1.9 +
    1.10 +lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n"
    1.11 +  by (simp add: numeral_eq_Suc)
    1.12 +
    1.13  lemma max_Suc_numeral [simp]:
    1.14    "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))"
    1.15    by (simp add: numeral_eq_Suc)