# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1609549532 -32400
# Node ID 4b6063ad6de20c6c36d121db00525a77981dd448
# Parent  ba7d4cc92e608dac5b04326549e4ec319a089947
...

diff -r ba7d4cc92e60 -r 4b6063ad6de2 agda/gcd.agda
--- a/agda/gcd.agda	Sat Jan 02 04:29:20 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 10:05:32 2021 +0900
@@ -117,8 +117,20 @@
 gcd11 : ( i  : ℕ ) → gcd i i ≡ i
 gcd11 i = gcdmm i i 
 
+gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
+gcd203 zero = refl
+gcd203 (suc i) = gcd205 (suc i) where
+   gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
+   gcd205 zero = refl
+   gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)
+gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
+gcd204 zero = refl
+gcd204 (suc zero) = refl
+gcd204 (suc (suc zero)) = refl
+gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) 
+
 gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
-gcd2 i j = gcd200 i i j j where
+gcd2 i j = gcd200 i i j j refl refl where
        gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
        gcd202 zero j1 = refl
        gcd202 (suc i) j1 = cong suc (gcd202 i j1)
@@ -129,14 +141,20 @@
           gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
           gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
           gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
-       gcd200 : (i i0 j j0 : ℕ) → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
-       gcd200 i i0 zero j0 = {!!}
-       gcd200 (suc (suc i)) i0 (suc j) (suc j0) = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
-       gcd200 zero zero (suc zero) j0 = {!!}
-       gcd200 zero zero (suc (suc j)) j0 = {!!}
-       gcd200 zero (suc i0) (suc j) j0 = {!!}
-       gcd200 (suc zero) i0 (suc j) j0 = {!!}
-       gcd200 (suc (suc i)) i0 (suc j) zero = {!!}
+       gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
+       gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl 
+       gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
+       gcd200 zero zero (suc zero) .1 i=i0 refl = refl
+       gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin
+          gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩
+          suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩
+          gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning
+       gcd200 zero (suc i0) (suc j) .(suc j) () refl
+       gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin
+          gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩
+          1 ≡⟨ sym ( gcd204 (suc j)) ⟩
+          gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
+       gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
 
 gcd4 : ( n k : ℕ ) → gcd n k ≡ k → k ≤ n
 gcd4 n k gn = gcd40 n n k k gn where