diff --git a/src/Connectives.lagda b/src/Connectives.lagda
index 81b2328e..203347b3 100644
--- a/src/Connectives.lagda
+++ b/src/Connectives.lagda
@@ -770,11 +770,12 @@ embedding, revealing a sense in which one of these laws is "more
 true" than the other.
 
 
-### Exercise (`×⊎-implies-⊎×`)
+### Exercise (`⊎×-implies-×⊎`)
 
-Show that a conjunct of disjuncts implies a disjunct of conjuncts.
+Show that a disjunct of conjuncts implies a conjunct of disjuncts.
 \begin{code}
-×⊎-Implies-⊎× = ∀ {A B C D : Set} → (A ⊎ B) × (C ⊎ D) → (A × C) ⊎ (B × D)
+postulate
+  ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
 \end{code}
 Does the converse hold? If so, prove; if not, explain why.
 
diff --git a/src/Naturals.lagda b/src/Naturals.lagda
index 86f95c3f..57e431f5 100644
--- a/src/Naturals.lagda
+++ b/src/Naturals.lagda
@@ -82,8 +82,8 @@ zero or more *judgments* written above a horizontal line, called the
 *conclusion*.  The first rule is the base case. It has no hypotheses,
 and the conclusion asserts that `zero` is a natural.  The second rule
 is the inductive case. It has one hypothesis, which assumes that `m`
-is a natural, and the conclusion asserts that `suc n` is a also a
-natural.
+is a natural, and in that case the conclusion asserts that `suc n`
+is a also a natural.
 
 
 ## Unpacking the Agda definition