asdf

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}