diff --git a/src/Exercises.lagda b/src/Exercises.lagda
new file mode 100644
index 00000000..45852c45
--- /dev/null
+++ b/src/Exercises.lagda
@@ -0,0 +1,73 @@
+---
+title     : "Exercises: Exercises"
+layout    : page
+permalink : /Exercises
+---
+
+## Imports
+
+\begin{code}
+open import Data.Nat using (ℕ; suc; zero; _+_; _*_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
+\end{code}
+
+## Exercises
+
+\begin{code}
+_∸_ : ℕ → ℕ → ℕ
+m       ∸ zero     =  m         -- (vii)
+zero    ∸ (suc n)  =  zero      -- (viii)
+(suc m) ∸ (suc n)  =  m ∸ n     -- (ix)
+
+infixl 6 _∸_
+
+assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+assoc+ zero n p = refl
+assoc+ (suc m) n p rewrite assoc+ m n p = refl
+
+com+zero : ∀ (n : ℕ) → n + zero ≡ n
+com+zero zero = refl
+com+zero (suc n) rewrite com+zero n = refl
+
+com+suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
+com+suc m zero = refl
+com+suc m (suc n) rewrite com+suc m n = refl
+
+com+ : ∀ (m n : ℕ) → m + n ≡ n + m
+com+ zero n rewrite com+zero n = refl
+com+ (suc m) n rewrite com+suc m n | com+ m n = refl
+
+dist*+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+dist*+ zero n p = refl
+dist*+ (suc m) n p rewrite dist*+ m n p | assoc+ p (m * p) (n * p) = refl
+
+assoc* : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
+assoc* zero n p = refl
+assoc* (suc m) n p rewrite dist*+ n (m * n) p | assoc* m n p = refl
+
+com*zero : ∀ (n : ℕ) → n * zero ≡ zero
+com*zero zero = refl
+com*zero (suc n) rewrite com*zero n = refl
+
+swap+ : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+swap+ m n p rewrite sym (assoc+ m n p) | com+ m n | assoc+ n m p = refl
+
+com*suc : ∀ (m n : ℕ) → n * suc m ≡ n + n * m
+com*suc m zero = refl
+com*suc m (suc n) rewrite com*suc m n | swap+ m n (n * m) = refl
+
+com* : ∀ (m n : ℕ) → m * n ≡ n * m
+com* zero n rewrite com*zero n = refl
+com* (suc m) n rewrite com*suc m n | com* m n = refl
+
+zero∸ : ∀ (n : ℕ) → zero ∸ n ≡ zero
+zero∸ zero = refl
+zero∸ (suc n) = refl
+
+assoc∸ : ∀ (m n p : ℕ) → (m ∸ n) ∸ p ≡ m ∸ (n + p)
+assoc∸ m zero p = refl
+assoc∸ zero (suc n) p rewrite zero∸ p = refl
+assoc∸ (suc m) (suc n) p rewrite assoc∸ m n p = refl
+\end{code}
+
+
diff --git a/src/Properties.lagda b/src/Properties.lagda
index 4db9e72e..aca3a909 100644
--- a/src/Properties.lagda
+++ b/src/Properties.lagda
@@ -229,9 +229,9 @@ induction hypothesis.
 
 We encode this proof in Agda as follows.
 \begin{code}
--- assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
--- assoc+ zero n p = refl
--- assoc+ (suc m) n p rewrite assoc+ m n p = refl
+assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+assoc+ zero n p = refl
+assoc+ (suc m) n p rewrite assoc+ m n p = refl
 \end{code}
 Here we have named the proof `assoc+`.  In Agda, identifiers can consist of
 any sequence of characters not including spaces or the characters `@.(){};_`.
@@ -564,6 +564,7 @@ com+suc m (suc n) rewrite com+suc m n = refl
 com : ∀ (m n : ℕ) → m + n ≡ n + m
 com zero n rewrite com+zero n = refl
 com (suc m) n rewrite com+suc m n | com m n = refl
+
 \end{code}
 Here we have renamed Lemma (x) and (xi) to `com+zero` and `com+suc`,
 respectively.  In the final line, rewriting with two equations
@@ -571,6 +572,9 @@ respectively.  In the final line, rewriting with two equations
 separating the two proofs of the relevant equations by a vertical bar;
 the rewrites on the left is performed before that on the right.
 
+## Exercises
+
+