From 49ab24195e358f2f4eb2ce80682776d0e47b3395 Mon Sep 17 00:00:00 2001
From: Felix Cherubini <felix.cherubini@posteo.de>
Date: Fri, 2 Aug 2024 18:11:33 +0200
Subject: [PATCH] make one example more meaningful

---
 Cubical/Tactics/CommRingSolver/Examples.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Tactics/CommRingSolver/Examples.agda b/Cubical/Tactics/CommRingSolver/Examples.agda
index 6d38ab13d5..531af32e9a 100644
--- a/Cubical/Tactics/CommRingSolver/Examples.agda
+++ b/Cubical/Tactics/CommRingSolver/Examples.agda
@@ -65,7 +65,7 @@ module Test (R : CommRing ℓ) (x y z : fst R) where
   ex1 : x ≡ x
   ex1 = solve! R
 
-  ex2 : x ≡ x
+  ex2 : (0r - 1r) · x ≡ 0r - x
   ex2 = solve! R
 
   ex3 : x + y ≡ y + x