--- a/automaton-in-agda/src/root2.agda	Thu Jun 17 17:16:36 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Thu Jun 17 22:42:36 2021 +0900
@@ -53,12 +53,11 @@
 
 open Factor
 
--- gcd-div : ( i j k : ℕ ) → (if : Factor k i) (jf : Factor k j )
---    → remain if ≡ 0 → remain jf ≡  0
+-- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
 
 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 = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) {!!} {!!} ) where 
+root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-div n m 2 (s≤s (s≤s z≤n)) dn dm ) where 
     rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
     rot13 d refl with Dividable.factor d | Dividable.is-factor d
     ... | zero | ()
@@ -112,5 +111,9 @@
          Even.j E * 2  ≡⟨  *-comm (Even.j E) 2  ⟩
          2 * Even.j E  ≡⟨  sym ( Even.is-twice E )  ⟩
          m ∎  where open ≡-Reasoning
+    dn : Dividable 2 n
+    dn = record { factor = factor f2 ; is-factor = subst (λ k → factor f2 * 2 + k ≡ n ) (f3 n rot7) (is-factor f2)  }
+    dm : Dividable 2 m
+    dm = record { factor = factor fm ; is-factor = is-factor fm }