--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/Reasoning.agda	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,21 @@
+open import Relation.Binary.PropositionalEquality
+open import nat
+open import nat_add
+open ≡-Reasoning
+
+module nat_add_sym_reasoning where
+
+addToRight : (n m : Nat) -> S (n + m) ≡ n + (S m)
+addToRight O m     = refl
+addToRight (S n) m = cong S (addToRight n m)
+
+addSym : (n m : Nat) -> n + m ≡ m + n
+addSym O       O   = refl
+addSym O    (S m)  = cong S (addSym O m)
+addSym (S n)   O   = cong S (addSym n O)
+addSym (S n) (S m) = begin
+  (S n) + (S m)  ≡⟨ refl ⟩
+  S (n + S m)    ≡⟨ cong S (addSym n (S m)) ⟩
+  S ((S m) + n)  ≡⟨ addToRight (S m) n ⟩
+  S (m + S n)    ≡⟨ refl ⟩
+  (S m) + (S n)  ∎