--- a/automaton-in-agda/src/root2.agda	Sun Jun 13 22:14:04 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Mon Jun 14 00:25:04 2021 +0900
@@ -53,10 +53,11 @@
 open Factor
 
 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-gt n n m m 2 f2 f2 f2 fm {!!} {!!} {!!} {!!}) where 
+root2-irrational n m n>1 m>1 2nm = rot13 ( gcd-gt n n m m 2 f2 f2 f2 fm (f3 n rot7) refl f4 f4) where 
     rot13 : {m : ℕ } → Dividable 2 m →  m ≡ 1 → ⊥
-    rot13 d refl with Dividable.is-factor d
-    ... | t = {!!}
+    rot13 d refl with Dividable.factor d | Dividable.is-factor d
+    ... | zero | ()
+    ... | suc n | ()
     rot11 : {m : ℕ } → even m → Factor 2 m 
     rot11 {zero} em = record { factor = 0 ; remain = 0 ; is-factor = refl }
     rot11 {suc zero} ()
@@ -95,6 +96,21 @@
     rot7 =  even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))
     f2 : Factor 2 n
     f2 = rot11 rot7
+    f3 : ( n : ℕ) → (e : even n ) →  remain (rot11 {n} e)  ≡ 0
+    f3 zero e = refl
+    f3 (suc (suc n)) e = f3 n e 
+    f4 : {m : ℕ} → remain f2 + m ≡ m
+    f4 {m} = begin
+        remain f2 + m ≡⟨ cong (λ k → k + m) (f3 n rot7)  ⟩
+        0 + m ≡⟨  refl  ⟩
+        m ∎  where open ≡-Reasoning
     fm : Factor 2 m
-    fm = record { factor = Even.j E ; remain = 0 ; is-factor = {!!} }
+    fm = record { factor = Even.j E ; remain = 0 ; is-factor = fm1 } where
+       fm1 : Even.j E * 2 + 0 ≡ m
+       fm1 = begin
+         Even.j E * 2 + 0 ≡⟨ +-comm _ 0  ⟩
+         Even.j E * 2  ≡⟨  *-comm (Even.j E) 2  ⟩
+         2 * Even.j E  ≡⟨  sym ( Even.is-twice E )  ⟩
+         m ∎  where open ≡-Reasoning
 
+