# HG changeset patch
# User haftmann
# Date 1587017370 -7200
# Node ID 2e3fa4e7cd73f87c20035ab69c08d895fee94720
# Parent  02c50bba930442f391c007f0ad8a31573a01640a
another rule on numerals

diff -r 02c50bba9304 -r 2e3fa4e7cd73 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Thu Apr 16 08:09:29 2020 +0200
+++ b/src/HOL/Num.thy	Thu Apr 16 08:09:30 2020 +0200
@@ -739,6 +739,17 @@
 lemma mult_minus1_right [simp]: "z * - 1 = - z"
   by (simp add: numeral.simps)
 
+lemma minus_sub_one_diff_one [simp]:
+  \<open>- sub m One - 1 = - numeral m\<close>
+proof -
+  have \<open>sub m One + 1 = numeral m\<close>
+    by (simp flip: eq_diff_eq add: diff_numeral_special)
+  then have \<open>- (sub m One + 1) = - numeral m\<close>
+    by simp
+  then show ?thesis
+    by simp
+qed
+
 end