--- a/agda/root2.agda	Sun Dec 27 13:26:44 2020 +0900
+++ b/agda/root2.agda	Mon Dec 28 11:35:29 2020 +0900
@@ -53,18 +53,24 @@
        2
     ∎ where open ≡-Reasoning
 
-gcd22 : { n m : ℕ} → gcd n 2 ≡ 2 → gcd m 2 ≡ 2 → ¬ ( gcd n m ≡ 1 )
-gcd22 {zero} {suc zero} gn () gnm
-gcd22 {zero} {suc (suc m)} refl gm ()
-gcd22 {suc zero} {zero} () gm gnm
-gcd22 {suc (suc n)} {zero} gn refl ()
-gcd22 {suc (suc n)} {suc (suc m)} gn gm gnm = gcd23 (suc n) (suc m) 0 {!!} gn gm gnm where
-   gcd12 : (n i : ℕ) →  gcd1 n (suc n) (suc i) 2 ≡ 2 →  gcd1 n (suc n) (suc i) 2 ≡ 2
-   gcd12 = ?
-   gcd23 : (n m i : ℕ ) → i ≤ 2  → (gn  : gcd1 n (suc n) (suc i) 2 ≡ 2) → (gm  : gcd1 m (suc m) (suc i) 2 ≡ 2) →
-       (gnm : gcd1 n (suc n) m (suc m) ≡ 1 ) → ⊥
-   gcd23 = {!!}
+open import nat
 
+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
+   gcd22 zero i0 zero o0 = refl
+   gcd22 zero i0 (suc o) o0 = refl
+   gcd22 (suc i) i0 zero o0 = refl
+   gcd22 (suc i) i0 (suc o) o0 = refl 
+   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 (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 = 
+       gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
+                                        (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)
 
 record Even (i : ℕ) : Set where
   field
@@ -135,8 +141,10 @@
     i j : ℕ
     coprime : gcd i j ≡ 1
 
-root2-irrational : ( n m : ℕ ) → n > 0 → m > 0  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
-root2-irrational n m n>0 m>0 2nm = gcd22 {n} {m}  (even→gcd=2 rot7 n>0 ) (even→gcd=2 ( even^2 {m} ( rot1)) m>0) where
+root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
+root2-irrational n m n>1 m>1 2nm = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
+    rot5 : {n : ℕ} → n > 1 → n > 0
+    rot5 {n} lt = <-trans a<sa lt 
     rot1 : even ( m * m )
     rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
        rot4 : (n * n) * 2 ≡ m * m