diff --git a/src/Properties.lagda b/src/Properties.lagda
index ab5caf6f..b4cafee1 100644
--- a/src/Properties.lagda
+++ b/src/Properties.lagda
@@ -217,7 +217,7 @@ be shown, and reading down from the top and up from the bottom takes us to
 
 For the inductive case, we must show:
 
-    (suc m + n) + p ≡ (suc m + n) + p
+    (suc m + n) + p ≡ suc m + (n + p)
 
 Simplifying both sides with the inductive case of addition yields the equation: