# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1609573894 -32400
# Node ID 0b74851665ee00173ef8d5ac05c25dad1a8c5a34
# Parent  91265c9712004a198a264c61d55ac1b66d6cd4fb
( n k : ℕ ) → 1 < n → gcd n k ≤ n

diff -r 91265c971200 -r 0b74851665ee agda/gcd.agda
--- a/agda/gcd.agda	Sat Jan 02 11:49:44 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 16:51:34 2021 +0900
@@ -35,9 +35,9 @@
 
 gcd1 : ( i i0 j j0 : ℕ ) → ℕ
 gcd1 zero i0 zero j0 with <-cmp i0 j0
-... | tri< a ¬b ¬c = j0
+... | tri< a ¬b ¬c = i0
 ... | tri≈ ¬a refl ¬c = i0
-... | tri> ¬a ¬b c = i0
+... | tri> ¬a ¬b c = j0
 gcd1 zero i0 (suc zero) j0 = 1
 gcd1 zero zero (suc (suc j)) j0 = j0
 gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
@@ -156,18 +156,25 @@
           gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
        gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()
 
-gcd6 : ( i i0 j j0 n n0 : ℕ) → gcd1 i i0 j j0 ≡  gcd1 0 n 0 n0 → n ≡ n0
-gcd6 i i0 j j0 n n0 = {!!} 
-
 gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n
 gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl where
+    gcd52 : {i : ℕ } → 1 < suc (suc i)
+    gcd52 {zero} = a<sa
+    gcd52 {suc i} = <-trans (gcd52 {i}) a<sa
     gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 →  gcd1 i i0 j j0 ≤ i0 
     gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0
-    ... | tri< a ¬b ¬c = {!!} -- ≤-refl    -- j0 ≤ i0
-    ... | tri≈ ¬a refl ¬c =  ≤-refl
-    ... | tri> ¬a ¬b c = ≤-refl
-    gcd50 zero i0 (suc j) j0 0<i  i<i0 j<j0 = {!!}
-    gcd50 (suc i) i0 j j0 0<i  i<i0 j<j0 = {!!}
+    ... | tri< a ¬b ¬c = ≤-refl    
+    ... | tri≈ ¬a refl ¬c =  ≤-refl 
+    ... | tri> ¬a ¬b c = ≤-trans refl-≤s c  
+    gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where 
+       gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0
+       gcd51 1<i = ≤to< 1<i
+    gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s
+    gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = ≤to< 0<i
+    gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl
+    gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i))  j0 (suc j0) gcd52  refl-≤s refl-≤s) i<i0
+    gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0))
+        (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) 
 
 gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
 gcd4 = {!!}