# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1609223577 -32400
# Node ID f896c112f01f8d105e6f22996f759e483a5a3983
# Parent  3294dbcccfe8772671ed651fec597c7f7535f0e8
...

diff -r 3294dbcccfe8 -r f896c112f01f agda/root2.agda
--- a/agda/root2.agda	Mon Dec 28 11:35:29 2020 +0900
+++ b/agda/root2.agda	Tue Dec 29 15:32:57 2020 +0900
@@ -55,6 +55,9 @@
 
 open import nat
 
+gcd24' : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
+gcd24' = {!!}
+
 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
    gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
@@ -62,10 +65,16 @@
    gcd22 zero i0 (suc o) o0 = refl
    gcd22 (suc i) i0 zero o0 = refl
    gcd22 (suc i) i0 (suc o) o0 = refl 
+   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 .1 zero j0 o o0 1<i 1<j 1<o gn gm refl = nat-<≡ 1<i
-   gcd21 zero i0 (suc zero) j0 o o0 1<i 1<j 1<o refl gm refl = {!!}
-   gcd21 zero i0 (suc (suc j)) j0 o o0 1<i 1<j 1<o refl gm gnm = {!!}
+   gcd21 zero i0 (suc zero) j0 zero o0 1<i 1<j 1<o refl gm gnm = nat-≡< gm 1<i
+   gcd21 zero (suc i0) (suc (suc j)) j0 zero (suc o0) 1<i 1<j 1<o refl gm gnm = {!!} where
+      gcd23 : gcd1 (suc j) (suc (suc j)) o0 (suc o0) ≡ suc i0 → gcd1 i0 (suc i0) (suc j) (suc (suc j)) ≡ 1 → ⊥
+      gcd23 = {!!}
+   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = ⊥-elim ( nat-<≡ 1<k )
+   gcd21 zero i0 (suc j) j0 (suc (suc 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 refl 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 =