--- a/automaton-in-agda/src/nat.agda	Fri Jun 18 10:04:11 2021 +0900
+++ b/automaton-in-agda/src/nat.agda	Fri Jun 18 17:55:41 2021 +0900
@@ -351,6 +351,10 @@
        suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩
        suc y + z ∎  ) where open ≡-Reasoning
 
+m*1=m : {m : ℕ } → m * 1 ≡ m
+m*1=m {zero} = refl
+m*1=m {suc m} = cong suc m*1=m
+
 record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
   field
     fzero   : {p : P} → f p ≡ zero → Q p

--- a/automaton-in-agda/src/prime.agda	Fri Jun 18 10:04:11 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 18 17:55:41 2021 +0900
@@ -99,15 +99,23 @@
      fact1 zero = init
      fact1 (suc m) = record { f1 = fact2 ; is-f1 = fact3 }  where
         fact2 : (n : ℕ ) →  0 < n →  n < suc (suc (suc m )) → ℕ
-        fact2 (suc j)  with <-cmp n j
-        ... | tri< a ¬b ¬c = {!!}
-        ... | tri≈ ¬a refl ¬c = {!!}
-        ... | tri> ¬a ¬b c = {!!}
+        fact2 (suc zero) 0<n n<m = factorial (suc (suc m))
+        fact2 (suc (suc n)) (s≤s 0<n) n<m  with <-cmp (suc n) (suc m)
+        ... | tri< a ¬b ¬c = F.f1 (fact1 m) (suc n) (s≤s z≤n) (≤-trans a refl-≤s) -- suc (suc n) ≤ suc m → suc n < suc (suc m)
+        ... | tri≈ ¬a refl ¬c = F.f1 (fact1 m) (suc m) (s≤s z≤n) a<sa * suc m
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s c) n<m ) -- suc (suc m) ≤ suc n
         fact3 : (n : ℕ ) (0<n : 0 < n) (n<m : n < suc (suc (suc m))) → fact2 n 0<n n<m * n ≡ factorial (suc (suc m))
-        fact3 n 0<n n<m  with <-cmp n {!!}
+        fact3 n 0<n n<m with  fact2 n 0<n n<m | inspect (fact2 n 0<n ) n<m  
+        fact3 (suc zero) 0<n n<m     | t | record { eq = refl } = m*1=m
+        fact3 (suc (suc n))  0<n n<m | t | record { eq = eq1 }  with <-cmp (suc n) (suc m)
         ... | tri< a ¬b ¬c = {!!}
-        ... | tri≈ ¬a b ¬c = {!!}
-        ... | tri> ¬a ¬b c = {!!}
+        ... | tri≈ ¬a refl ¬c = begin
+            t * suc (suc m) ≡⟨ cong ( λ k → k * suc (suc m)) (sym eq1) ⟩
+            fact2 (suc (suc n)) 0<n n<m * suc (suc n) ≡⟨ {!!} ⟩
+            suc (suc m) * (F.f1 (fact1 m) (suc m) (s≤s z≤n) a<sa * suc m) ≡⟨ cong ( λ k → suc (suc m) * k ) (F.is-f1 (fact1 m) (suc n) (s≤s z≤n) a<sa) ⟩
+            suc (suc m) * factorial (suc m) ≡⟨ refl ⟩
+            factorial (suc (suc m)) ∎  where open ≡-Reasoning
+        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s c) n<m ) -- suc (suc m) ≤ suc n
      last :  F.f1 (fact1 m) n 0<n n<m * n + 0 ≡ factorial (suc m)
      last = begin
          F.f1 (fact1 m ) n 0<n n<m * n + 0 ≡⟨ +-comm _ 0 ⟩