diff --git a/talks/2024-grads/Demo.agda b/talks/2024-grads/Demo.agda
index 3258560..b344d9e 100644
--- a/talks/2024-grads/Demo.agda
+++ b/talks/2024-grads/Demo.agda
@@ -1,14 +1,20 @@
 module 2024-grads.Demo where
 
 open import Data.Nat
+open import Data.Nat.Properties
+open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.PropositionalEquality using (module ≡-Reasoning)
 open import Tactic.RingSolver.Core.AlmostCommutativeRing using (AlmostCommutativeRing)
 open import Data.Nat.Tactic.RingSolver
+open ≡-Reasoning
 
 sumTo : ℕ → ℕ
 sumTo zero = zero 
 sumTo (suc n) = (suc n) + (sumTo n)
 
+lemma : ∀ (n : ℕ) → 2 * suc n + n * (n + 1) ≡ suc n * (suc n + 1)
+lemma = solve-∀
+
 theorem : ∀ (n : ℕ) → 2 * sumTo n ≡ (n * (n + 1))
 theorem zero = refl 
 theorem (suc n) =
@@ -21,6 +27,6 @@ theorem (suc n) =
         2 * (suc n) + 2 * (sumTo n)
     ≡⟨ cong (2 * (suc n) +_) IH ⟩
         2 * (suc n) + (n * (n + 1))
-    ≡⟨ {!  solve-∀ !} ⟩
+    ≡⟨ lemma n ⟩
         (suc n) * ((suc n) + 1)
-    ∎
\ No newline at end of file
+    ∎