equal
deleted
inserted
replaced
917 by (simp add: numeral_eq_Suc) |
917 by (simp add: numeral_eq_Suc) |
918 |
918 |
919 lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k" |
919 lemma le_Suc_numeral [simp]: "Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k" |
920 by (simp add: numeral_eq_Suc) |
920 by (simp add: numeral_eq_Suc) |
921 |
921 |
|
922 lemma diff_Suc_numeral [simp]: "Suc n - numeral k = n - pred_numeral k" |
|
923 by (simp add: numeral_eq_Suc) |
|
924 |
|
925 lemma diff_numeral_Suc [simp]: "numeral k - Suc n = pred_numeral k - n" |
|
926 by (simp add: numeral_eq_Suc) |
|
927 |
922 lemma max_Suc_numeral [simp]: |
928 lemma max_Suc_numeral [simp]: |
923 "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))" |
929 "max (Suc n) (numeral k) = Suc (max n (pred_numeral k))" |
924 by (simp add: numeral_eq_Suc) |
930 by (simp add: numeral_eq_Suc) |
925 |
931 |
926 lemma max_numeral_Suc [simp]: |
932 lemma max_numeral_Suc [simp]: |