--- a/src/HOL/Groups.thy Fri Nov 08 20:59:34 2019 +0100
+++ b/src/HOL/Groups.thy Sat Nov 09 10:38:51 2019 +0000
@@ -606,6 +606,10 @@
"(a - b) + c = (a + c) - b"
by (simp add: algebra_simps)
+lemma minus_diff_commute:
+ "- b - a = - a - b"
+ by (simp only: diff_conv_add_uminus add.commute)
+
end