--- a/agda/chap0.agda	Thu Oct 17 15:11:39 2019 +0900
+++ b/agda/chap0.agda	Thu Oct 17 20:00:26 2019 +0900
@@ -184,14 +184,15 @@
 
 dgree-even : ( g : List ( ℕ × ℕ )) → sum-of-dgree g % 2 ≡ 0
 dgree-even [] = refl
-dgree-even ((e , e1) ∷ t) with dgree-even t
-... | s = subst (λ k → k % 2 ≡ 0 ) (sym lemma)( even2 (sum-of-dgree t) s ) where
-   lemma : sum-of-dgree ((e , e1) ∷ t) ≡ sum-of-dgree t + 2
-   lemma = begin
-         sum-of-dgree ((e , e1) ∷ t)
-      ≡⟨⟩
-         2 + sum-of-dgree t 
-      ≡⟨ +-comm 2 _ ⟩
-         sum-of-dgree t + 2
-     ∎ where open ≡-Reasoning
+dgree-even ((e , e1) ∷ t) = begin
+      sum-of-dgree ((e , e1) ∷ t) % 2
+   ≡⟨⟩
+      (2 + sum-of-dgree t ) % 2
+   ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) ) ⟩
+      (sum-of-dgree t + 2) % 2
+   ≡⟨ [a+n]%n≡a%n (sum-of-dgree t) _  ⟩
+      sum-of-dgree t % 2
+   ≡⟨ dgree-even t ⟩
+      0
+   ∎ where open ≡-Reasoning
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/root2.agda	Thu Oct 17 20:00:26 2019 +0900
@@ -0,0 +1,34 @@
+module root2 where
+
+open import Data.Nat
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat.DivMod
+
+even : (n : ℕ ) → Set
+even n =  n % 2 ≡ 0 
+
+even? : (n : ℕ ) → Dec ( even n )
+even? n with n % 2
+even? n | zero = yes refl
+even? n | suc k = no ( λ () )
+
+nn-even : {n : ℕ } → even n → even ( n * n )
+nn-even {n} eq = {!!}
+
+2-even : {n : ℕ } → even ( 2 * n )
+2-even {n} = {!!}
+
+even-2 : (n : ℕ ) → (n + 2) % 2 ≡ 0 → n % 2 ≡ 0 
+even-2 0 refl = refl
+even-2 1 () 
+even-2 (suc (suc n)) eq = {!!} -- trans ([a+n]%n≡a%n (suc (suc n)) _ ) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
+
+even-half : (n : ℕ ) → even n → ℕ 
+even-half zero _ = zero
+even-half (suc (suc n)) ev = {!!} -- 1 + even-half n (subst (λ k → k ≡ 0 ) {!!} {!!} )
+
+root2-irrational : ( n m : ℕ ) → ¬ ( 2 * n * n ≡ m * m )
+root2-irrational n m eq = {!!}
+