diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index f625339518..4c1b44bab4 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -410,7 +410,8 @@ section add_group
 
   theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
 
-  theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▸ rfl
+  theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b :=
+  by change a + -(-b) = a + b; rewrite neg_neg
 
   theorem neg_sub (a b : A) : -(a - b) = b - a :=
   neg_eq_of_add_eq_zero
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 66c372c5d0..01f9427aaf 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -433,7 +433,8 @@ section add_group
 
   theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
 
-  theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▸ rfl
+  theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b :=
+  by change a + -(-b) = a + b; rewrite neg_neg
 
   theorem neg_sub (a b : A) : -(a - b) = b - a :=
   neg_eq_of_add_eq_zero