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