--- a/agda/gcd.agda	Sat Jan 02 10:05:32 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 11:49:44 2021 +0900
@@ -156,22 +156,30 @@
           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
-       gcd40 :  (i i0 j j0 : ℕ) → gcd1 i i0 j j0 ≡ j0 → j0 ≤ i0
-       gcd40 zero i0 zero j0  gn = {!!}
-       gcd40 zero i0 (suc j) j0 gn = {!!}
-       gcd40 (suc i) i0 zero j0 gn = {!!}
-       gcd40 (suc i) i0 (suc j) j0 gn = gcd40 i i0 j j0 (subst (λ k → k ≡ j0) (gcd22 i i0 j j0) gn)
+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 = {!!} 
 
-gcd3 : ( n k : ℕ ) → n ≤ k + k → gcd n k ≡ k → n ≡ k
-gcd3 n k n<2k gn = {!!}
+gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n
+gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl where
+    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 = {!!}
 
-gcd23 : ( n m k : ℕ) → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
+gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
+gcd4 = {!!}
+
+gcd3 : ( n k : ℕ ) → 0 < n → n ≤ k + k → gcd n k ≡ k → n ≡ k
+gcd3 n k 0<n n<2k gn = {!!}
+
+gcd23 : ( n m k : ℕ) → 0 < n → 0 < m  → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
 gcd23 = {!!}
 
 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 = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k gn gm  )))
+gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = ⊥-elim ( nat-≡< (sym gnm) (≤-trans 1<k (gcd23 n m k {!!} {!!} gn gm  )))
 
 record Even (i : ℕ) : Set where
   field