--- a/automaton-in-agda/src/root2.agda	Tue Jun 29 09:35:12 2021 +0900
+++ b/automaton-in-agda/src/root2.agda	Tue Jun 29 16:10:06 2021 +0900
@@ -29,12 +29,14 @@
 divdable^2 zero zero () 1<n pk dn2
 divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
 ... | yes y = y
-... | no non with gcd-equlid (suc k) (suc n) (suc n) 1<k (Prime.isPrime pk) dn2
+... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2 
 ... | case1 dn = dn
 ... | case2 dm = dm
 
 p2 : Prime 2
-  p2 = record { p>1 = a<sa ; isPrime = {!!} }
+p2 = record { p>1 = a<sa ; isPrime = p22 } where
+   p22 : (j : ℕ) → j < 2 → 0 < j → gcd 2 j ≡ 1
+   p22 1 (s≤s (s≤s z≤n)) (s≤s 0<j) = refl
 
 -- gcd-div : ( i j k : ℕ ) → (if : Dividable k i) (jf : Dividable k j )
 --    → Dividable k ( gcd i  j )
@@ -46,8 +48,23 @@
     ... | zero | ()
     ... | suc n | ()
     dm : Dividable 2 m
-    dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = {!!} }
+    dm = divdable^2 m 2 a<sa m>1 p2 record { factor = n * n ; is-factor = begin
+       (n * n) * 2 + 0 ≡⟨  +-comm _ 0 ⟩
+       (n * n) * 2  ≡⟨ *-comm (n * n) 2 ⟩
+       2 * (n * n)  ≡⟨ sym (*-assoc 2 n n)  ⟩
+       (2 * n) * n ≡⟨ 2nm  ⟩
+       m * m ∎ }  where open ≡-Reasoning
+    df = Dividable.factor dm
     dn : Dividable 2 n
-    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = Dividable.factor dm * m ; is-factor = {!!} }
+    dn = divdable^2 n 2 a<sa n>1 p2 record { factor = Dividable.factor dm * m ; is-factor = begin
+        df * m * 2 + 0  ≡⟨ *-cancelʳ-≡ _ _ {1} ( begin 
+          {!!}  ≡⟨  {!!} ⟩
+          ((df * m) * 2 )  ≡⟨  {!!} ⟩
+          ((m * df) * 2 )  ≡⟨  {!!} ⟩
+          (m * (df * 2) )  ≡⟨  {!!} ⟩
+          (m * (df * 2 + 0) )  ≡⟨  {!!} ⟩
+          m * m   ≡⟨  {!!} ⟩
+          n * n * 2 ∎  ) ⟩
+       n * n ∎ }  where open ≡-Reasoning