diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index f75643481..2157ccca0 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -427,7 +427,7 @@ section add_group
 
   theorem minus_zero (a : A) : a - 0 = a := (neg_zero⁻¹) ▹ !add_right_id
 
-  theorem minus_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg⁻¹ ▹ idp
+  theorem minus_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▹ idp
 
   theorem neg_minus_eq (a b : A) : -(a - b) = b - a :=
   neg_unique
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 9b0b2e9c3..577560137 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -424,7 +424,7 @@ 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 := !neg_neg ▸ rfl
 
   theorem neg_sub (a b : A) : -(a - b) = b - a :=
   neg_eq_of_add_eq_zero