From bf178e1b8b81f7a35853113e7ca6ebb0f9d63496 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 18 Sep 2021 14:44:20 -0500
Subject: [PATCH] asdf

---
 src/plfa/part1/Relations.lagda.md | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md
index 8d6f6bdb..87784a5d 100644
--- a/src/plfa/part1/Relations.lagda.md
+++ b/src/plfa/part1/Relations.lagda.md
@@ -754,7 +754,15 @@ successor of the sum of two even numbers, which is even.
 Show that the sum of two odd numbers is even.
 
 ```
--- Your code goes here
+import Data.Nat.Properties
+open Data.Nat.Properties using (+-suc)
+
+o+o≡e : ∀ {m n : ℕ}
+  → odd m → odd n
+  → even (m + n)
+
+-- o+o≡e om (suc en) = suc (+-suc (o+e≡o om en))
+o+o≡e om (suc en) = +-suc ?
 ```
 
 #### Exercise `Bin-predicates` (stretch) {name=Bin-predicates}