--- a/automaton-in-agda/src/prime.agda	Fri Jun 18 18:51:24 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Fri Jun 18 19:21:06 2021 +0900
@@ -87,13 +87,31 @@
      suc (factorial (suc m)) ∎  where open ≤-Reasoning
   fact< : (m n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
   fact< zero 1 0<n (s≤s (s≤s z≤n)) = record { factor = 1 ; is-factor = refl }
-  fact< (suc m) (suc zero) 0<n n<m = record { factor = factorial (suc (suc m)) ; is-factor = {!!} }
+  fact< (suc m) (suc zero) 0<n n<m = record { factor = factorial (suc (suc m)) ; is-factor = begin
+     factorial (suc (suc m)) * 1 + 0  ≡⟨ +-comm _ 0 ⟩
+     factorial (suc (suc m)) * 1   ≡⟨ m*1=m  ⟩
+     (suc (suc m)) * factorial (suc m)  ≡⟨ refl ⟩
+     factorial (suc (suc m))  ∎  } where open ≡-Reasoning
   fact< (suc m) (suc (suc n)) 0<n n<m with <-cmp (suc (suc n)) (suc (suc m))
-  ... | tri< a ¬b ¬c = record { factor = suc (suc m) * Dividable.factor fact1 ; is-factor = {!!} } where
+  ... | tri< a ¬b ¬c = record { factor = suc (suc m) * Dividable.factor fact1 ; is-factor = fact2 } where
       fact1 : Dividable (suc (suc n))  (factorial (suc m ))
       fact1 = fact< m (suc (suc n)) 0<n a 
-  ... | tri≈ ¬a b ¬c = record { factor = factorial (suc m)  ; is-factor = {!!} }
-  ... | tri> ¬a ¬b c = {!!}
+      d =  (fact< m (suc (suc n)) 0<n a)
+      fact2 : suc (suc m) * Dividable.factor d * suc (suc n) + 0 ≡ factorial (suc (suc m))
+      fact2 = begin
+        suc (suc m) * Dividable.factor d * suc (suc n) + 0  ≡⟨ +-comm _ 0 ⟩
+        suc (suc m) * Dividable.factor d * suc (suc n)   ≡⟨ *-assoc (suc (suc m)) (Dividable.factor d) ( suc (suc n)) ⟩
+        suc (suc m) * (Dividable.factor d * suc (suc n))   ≡⟨ cong (λ k →  suc (suc m) * k ) ( +-comm 0 (Dividable.factor d * suc (suc n)) ) ⟩
+        suc (suc m) * (Dividable.factor d * suc (suc n) + 0)   ≡⟨ cong (λ k → suc (suc m) * k ) (Dividable.is-factor d)  ⟩
+        suc (suc m) * factorial (suc m)  ≡⟨ refl ⟩
+        factorial (suc (suc m))  ∎   where open ≡-Reasoning
+  ... | tri≈ ¬a b ¬c = record { factor = factorial (suc m)  ; is-factor = begin
+     factorial (suc m) * suc (suc n) + 0 ≡⟨ +-comm _ 0 ⟩
+     factorial (suc m) * suc (suc n)  ≡⟨ *-comm (factorial (suc m)) (suc (suc n))  ⟩
+     (suc (suc n)) * factorial (suc m)  ≡⟨ cong (λ k → k * factorial (suc m) ) b ⟩
+     (suc (suc m)) * factorial (suc m)  ≡⟨ refl ⟩
+     factorial (suc (suc m))  ∎  } where open ≡-Reasoning
+  ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n<m) 
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
   fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( prime<max n p )
   -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)