From 583e0fb3440829af3b72f63b5c3c76dfbb7e17fa Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 9 Sep 2021 10:28:51 -0500
Subject: [PATCH] begin induction

---
 src/plfa/part1/Induction.lagda.md | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md
index 7d19138f..bcad53b1 100644
--- a/src/plfa/part1/Induction.lagda.md
+++ b/src/plfa/part1/Induction.lagda.md
@@ -868,7 +868,17 @@ just apply the previous results which show addition
 is associative and commutative.
 
 ```
--- Your code goes here
++-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
++-swap m n p =
+  begin
+    m + (n + p)
+  ≡⟨ sym (+-assoc m n p) ⟩
+    (m + n) + p
+  ≡⟨ cong (_+ p) (+-comm m n) ⟩
+    (n + m) + p
+  ≡⟨ +-assoc n m p ⟩
+    n + (m + p)
+  ∎
 ```
 
 
@@ -882,6 +892,9 @@ for all naturals `m`, `n`, and `p`.
 
 ```
 -- Your code goes here
+*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+ zero n p = {! begin (zero + n) * p ≡ zero * p + n * p ∎  !}
+*-distrib-+ (suc m) n p = {!   !}
 ```