--- a/agda/gcd.agda	Fri Jan 01 22:10:10 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 01:59:47 2021 +0900
@@ -52,12 +52,9 @@
 even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
 even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
 even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
-       gcd (suc (suc (suc (suc n)))) 2
-    ≡⟨⟩
-       gcd (suc (suc n)) 2
-    ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
-       2
-    ∎ where open ≡-Reasoning
+       gcd (suc (suc (suc (suc n)))) 2 ≡⟨⟩
+       gcd (suc (suc n)) 2 ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
+       2 ∎ where open ≡-Reasoning
 
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
@@ -68,6 +65,14 @@
 gcd22 (suc i) i0 zero o0 = refl
 gcd22 (suc i) i0 (suc o) o0 = refl 
 
+gcd20 : (i : ℕ) → gcd i 0 ≡ i
+gcd20 zero = refl
+gcd20 (suc i) = gcd201 (suc i) where
+    gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
+    gcd201 zero = refl
+    gcd201 (suc zero) = refl
+    gcd201 (suc (suc i)) = refl
+
 gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
 gcdmm zero m with <-cmp m m
 ... | tri< a ¬b ¬c = refl
@@ -81,9 +86,6 @@
        comp : ℕ
        is-comp : n * comp ≡ m
 
-gcd28 : (n m  : ℕ) → Comp n m → Comp (n bb
-gcd28 = ?
-
 gcd27 : (n m i : ℕ) → 1 < m  → gcd n i ≡ m → Comp m n ∨ Comp m i
 gcd27 n m i 1<m gn = gcd271 n n i i gn where
     gcd271 : (n n0 i i0 : ℕ ) → gcd1 n n0 i i0 ≡ m → Comp m n0 ∨ Comp m i0
@@ -96,13 +98,13 @@
     gcd271 zero (suc n0) (suc (suc i)) i0 eq with gcd271 n0 (suc n0) (suc i) (suc (suc i)) eq
     ... | case1 t = case1 t
     -- t : Comp m (suc (suc i)),    (suc n0) + (suc (suc i)) ≡ i0
-    ... | case2 t = case2 (record { non-1 = 1<m ; comp = suc (suc i) ; is-comp = subst (λ k → k ≡ m) {!!} eq })
+    ... | case2 t = case1 (gcd272 t) where
+      gcd272 : Comp m (suc (suc i)) → Comp m (suc n0)
+      gcd272 = {!!}
     gcd271 (suc zero) n0 zero i0 eq = ⊥-elim ( nat-≡< eq 1<m )
     gcd271 (suc (suc n)) n0 zero zero eq = case2 (record { non-1 = 1<m ; comp = n0 ; is-comp = subst (λ k → k ≡ m) {!!} eq })
     gcd271 (suc (suc n)) n0 zero (suc i0) eq = {!!}
-    gcd271 (suc n) n0 (suc i) i0 eq with gcd271 n n0 i i0 (trans (sym (gcd22 n n0 i i0)) eq )
-    ... | case1 x = case1 x
-    ... | case2 x = case2 x
+    gcd271 (suc n) n0 (suc i) i0 eq = gcd271 n n0 i i0 (trans (sym (gcd22 n n0 i i0)) eq )
 
 gcd26 : (n m i : ℕ) → 1 < n → 1 < m  → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
 gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
@@ -157,6 +159,24 @@
 gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
 gcdsym {n} {m} = gcdsym1 n n m m 
 
+gcd11 : ( i  : ℕ ) → gcd i i ≡ i
+gcd11 i = gcdmm i i 
+
+gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
+gcd2 zero zero = refl
+gcd2 zero (suc j) = begin
+       gcd (zero + suc j) (suc j) ≡⟨⟩
+       gcd (suc j) (suc j) ≡⟨ gcd11 (suc j) ⟩
+       suc j ≡⟨ sym (gcd20 (suc j)) ⟩
+       gcd (suc j) zero  ≡⟨ gcdsym {suc j} ⟩
+       gcd zero (suc j) ∎ where open ≡-Reasoning
+gcd2 (suc i) zero = begin
+       gcd (suc i + zero) zero ≡⟨ cong (λ k → gcd k zero) (+-comm (suc i) _ ) ⟩
+       gcd (suc i) zero ∎ where open ≡-Reasoning
+gcd2 (suc i) (suc j) = gcd200 (suc i) (suc i) (suc j) (suc j) where
+       gcd200 : (i i0 j j0 : ℕ) → gcd1 (i + j0) (i0 + j0) j j0 ≡ gcd1 i i0 j j0
+       gcd200 i i0 j j0 = {!!}
+
 gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
 gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
    gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0