--- a/agda/gcd.agda	Mon Jan 04 11:56:14 2021 +0900
+++ b/agda/gcd.agda	Mon Jan 04 12:52:04 2021 +0900
@@ -204,6 +204,8 @@
 
 gcd23 : ( n m k : ℕ) → 1 < n → 1 < m  → gcd n k ≡ k → gcd m k ≡ k → k ≤ gcd n m 
 gcd23 n m k 1<n 1<m gn gm = gcd230 n n m m k k 1<n 1<m ≤-refl ≤-refl ≤-refl gn gm where
+     gcd232 : (i i0 k k0 : ℕ) → (1 < i0) → i ≤ i0 → k ≤ k0 → gcd1 (suc i) i0 (suc k) k0 ≡ suc k → gcd1 i i0 (suc k) k0 ≡ suc k
+     gcd232 i i0 k k0 1<i0 i<i0 k<k0 = {!!}
      gcd231 : (i0 k k0 : ℕ) → (1 < i0) → (suc k ≤ k0) → gcd1 0 i0 (suc k) k0 ≡ suc k → suc k ≤ i0
      gcd231 i0 k k0 1<i0 sk<k0 gi = subst (λ m → m ≤ i0 ) gi ( gcd50 0 i0 (suc k) k0 1<i0 z≤n sk<k0 )
      gcd230 : (i i0 j j0 k k0 : ℕ) → 1 < i0 → 1 < j0 → i ≤ i0 → j ≤ j0 → k ≤ k0  → gcd1 i i0 k k0 ≡ k → gcd1 j j0 k k0 ≡ k → k ≤ gcd1 i i0 j j0