--- a/automaton-in-agda/src/prime.agda	Tue Jun 29 18:37:42 2021 +0900
+++ b/automaton-in-agda/src/prime.agda	Tue Jun 29 20:03:32 2021 +0900
@@ -101,60 +101,40 @@
     ... | tri> ¬a ¬b c    = np1 n m np 1<n (skipFactor n c) 
     ... | tri≈ ¬a refl ¬c = np1 n m np 1<n (findFactor m ≤-refl (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n) ))
 
-
-prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
-prime-is-infinite zero pmax = pmax 3 (s≤s z≤n) record { isPrime = λ n lt 0<j → pif3 n lt 0<j  ; p>1 = s≤s (s≤s z≤n) } where
-  pif3 : (n : ℕ) →  n < 3 →  0 < n → gcd 3 n ≡ 1
-  pif3 .1 (s≤s (s≤s z≤n)) _ = refl
-  pif3 .2 (s≤s (s≤s (s≤s z≤n))) _ = refl
-prime-is-infinite (suc m) pmax = newPrime where 
-  factorial : (n : ℕ) → ℕ
-  factorial zero = 1
-  factorial (suc n) = (suc n) * (factorial n)
-  prime<max : (n : ℕ ) → Prime n → n < suc (suc m)
-  prime<max n p with <-cmp n (suc m) 
-  ... | tri< a ¬b ¬c = ≤-trans a refl-≤s 
-  ... | tri≈ ¬a refl ¬c = ≤-refl 
-  ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p ) 
-  factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n)
-  factorial-mono n = begin
+factorial : (n : ℕ) → ℕ
+factorial zero = 1
+factorial (suc n) = (suc n) * (factorial n)
+factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n)
+factorial-mono n = begin
      factorial n  ≤⟨ x≤x+y ⟩
      factorial n + n * factorial n ≡⟨ refl ⟩
      (suc n) * factorial n  ≡⟨ refl ⟩
      factorial (suc n)  ∎  where open ≤-Reasoning
-  factorial≥1 : {m : ℕ} → 1 ≤ factorial m
-  factorial≥1 {zero} = ≤-refl
-  factorial≥1 {suc m} = begin
+factorial≥1 : {m : ℕ} → 1 ≤ factorial m
+factorial≥1 {zero} = ≤-refl
+factorial≥1 {suc m} = begin
      1 ≤⟨ s≤s z≤n ⟩
      (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
      (suc m) * factorial m ≡⟨ refl ⟩
      factorial (suc m)  ∎  where open ≤-Reasoning
-  m<factorial : (m : ℕ) → m ≤ factorial m
-  m<factorial zero = z≤n
-  m<factorial (suc m) = begin
+m<factorial : (m : ℕ) → m ≤ factorial m
+m<factorial zero = z≤n
+m<factorial (suc m) = begin
      suc m ≡⟨ cong suc (+-comm 0 _) ⟩
      1 * suc m ≡⟨ *-comm 1 _ ⟩
      (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
      (suc m) * factorial m  ≡⟨ refl ⟩
      factorial (suc m)  ∎  where open ≤-Reasoning
-  -- *-monoˡ-≤ (suc m) {!!}
-  f>m :  suc m < suc (factorial (suc m))
-  f>m = begin
-     suc (suc m)  ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩
-     suc (1 + 1 * m)  ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m)  ⟩
-     suc (1 + m * 1)  ≤⟨ s≤s (s≤s (*-monoʳ-≤ m  (factorial≥1 {m}) )) ⟩
-     suc (1 + m * factorial m) ≤⟨ s≤s  (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩
-     suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
-     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 = begin
+-- *-monoˡ-≤ (suc m) {!!}
+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 = 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 = fact2 } where
+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 = fact2 } where
       fact1 : Dividable (suc (suc n))  (factorial (suc m ))
       fact1 = fact< m (suc (suc n)) 0<n a 
       d =  (fact< m (suc (suc n)) 0<n a)
@@ -166,13 +146,34 @@
         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
+... | 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) 
+... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n<m) 
+
+f>m :  {m : ℕ} → suc m < suc (factorial (suc m))
+f>m {m} = begin
+     suc (suc m)  ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩
+     suc (1 + 1 * m)  ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m)  ⟩
+     suc (1 + m * 1)  ≤⟨ s≤s (s≤s (*-monoʳ-≤ m  (factorial≥1 {m}) )) ⟩
+     suc (1 + m * factorial m) ≤⟨ s≤s  (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩
+     suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
+     suc (factorial (suc m)) ∎  where open ≤-Reasoning
+
+prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
+prime-is-infinite zero pmax = pmax 3 (s≤s z≤n) record { isPrime = λ n lt 0<j → pif3 n lt 0<j  ; p>1 = s≤s (s≤s z≤n) } where
+  pif3 : (n : ℕ) →  n < 3 →  0 < n → gcd 3 n ≡ 1
+  pif3 .1 (s≤s (s≤s z≤n)) _ = refl
+  pif3 .2 (s≤s (s≤s (s≤s z≤n))) _ = refl
+prime-is-infinite (suc m) pmax = newPrime where 
+  prime<max : (n : ℕ ) → Prime n → n < suc (suc m)
+  prime<max n p with <-cmp n (suc m) 
+  ... | tri< a ¬b ¬c = ≤-trans a refl-≤s 
+  ... | tri≈ ¬a refl ¬c = ≤-refl 
+  ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p ) 
   fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
   fact n p = fact< m n (<-trans (s≤s z≤n) (Prime.p>1 p)) ( prime<max n p )
   -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)