--- a/agda/root2.agda	Tue Dec 29 15:38:52 2020 +0900
+++ b/agda/root2.agda	Tue Dec 29 17:53:40 2020 +0900
@@ -55,8 +55,9 @@
 
 open import nat
 
-gcd24' : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
-gcd24' = {!!}
+-- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
+-- gcd25 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd m n
+-- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
 
 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
@@ -65,12 +66,20 @@
    gcd22 zero i0 (suc o) o0 = refl
    gcd22 (suc i) i0 zero o0 = refl
    gcd22 (suc i) i0 (suc o) o0 = refl 
+   gcd23 : { j j0 : ℕ } → 1 < j → 1 < j0 → ¬ (gcd1 zero zero j j0 ≡ 1)
+   gcd23 {zero} {suc j0} 1<j 1<j0 ()
+   gcd23 {suc zero} {suc j0} 1<j 1<j0 gn = nat-<≡ 1<j
+   gcd23 {suc (suc j)} {suc .0} 1<j 1<j0 refl = nat-<≡ 1<j0
    1<ss : {j : ℕ} → 1 < suc (suc j)
    1<ss = s≤s (s≤s z≤n)
    gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
    gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) 1<i
-   gcd21 zero i0 (suc j) j0 o o0 1<i 1<j 1<o refl gm gnm = {!!}
-   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn refl gnm = {!!}
+   --- gcd1 zero i0 o o0 ≡ k    o = suc zero → k ≡ 1 
+   ---                          i0 = zero , o = suc (suc o) → o0 = k -> gcd1 zero zero (suc j) j0 ≡ 1
+   --                           i0 = suc i0, o = suc (suc o) → gn = gcd1 i0 (suc i0) (suc o) (suc (suc o))
+   gcd21 zero i0 (suc j) j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
+   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
+   -- ?
    gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
    gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
        gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)