--- a/agda/gcd.agda	Sat Jan 02 16:51:34 2021 +0900
+++ b/agda/gcd.agda	Sat Jan 02 18:23:54 2021 +0900
@@ -177,16 +177,19 @@
         (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 = {!!}
+gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n)
 
-gcd3 : ( n k : ℕ ) → 0 < n → n ≤ k + k → gcd n k ≡ k → n ≡ k
-gcd3 n k 0<n n<2k gn = {!!}
+gcd3 : ( n k : ℕ ) → 1 < n → n ≤ k + k → gcd n k ≡ k → n ≡ k
+gcd3 n k 1<n n<2k gn with gcd4 n k 1<n gn | <-cmp n k
+... | k≤n | tri< a ¬b ¬c = ⊥-elim (nat-≤> k≤n a)
+... | k≤n | tri≈ ¬a b ¬c = b
+... | k≤n | tri> ¬a ¬b c = ⊥-elim (nat-≤> k≤n  {!!} )
 
-gcd23 : ( n m k : ℕ) → 0 < n → 0 < m  → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
+gcd23 : ( n m k : ℕ) → 1 < n → 1 < 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 1<n 1<m gn gm  )))
 
 record Even (i : ℕ) : Set where
   field