diff --git a/examples/peano.pg b/examples/peano.pg
index ab728c6..fa09c90 100644
--- a/examples/peano.pg
+++ b/examples/peano.pg
@@ -360,3 +360,35 @@ plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m))
             (eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
               -- suc (n + m) = n + suc m
               (eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
+
+-- Finally, we can prove commutativity.
+plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
+  -- As usual, we proceed by induction.
+  nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
+
+  -- Base case: WTS n + 0 = 0 + n
+  -- n + 0 = n = 0 + n
+  (eq_trans nat (plus n zero) n (plus zero n)
+    -- n + 0 = n
+    (plus_0_r n)
+
+    -- n = 0 + n
+    (eq_sym nat (plus zero n) n (plus_0_l n)))
+
+  -- Inductive step:
+  (fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
+    -- WTS n + suc m = suc m + n
+    -- n + suc m = suc (n + m)
+    --           = suc (m + n)
+    --           = suc m + n
+    (eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
+      -- n + suc m = suc (n + m)
+      (plus_s_r n m)
+
+      -- suc (n + m) = suc m + n
+      (eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
+        -- suc (n + m) = suc (m + n)
+        (eq_cong nat nat (plus n m) (plus m n) suc IH)
+
+        -- suc (m + n) = suc m + n
+        (eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));