# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615596644 -32400
# Node ID c25b7de9cc358311e7a451a463e5c4eb13c31ba6
# Parent  fc770d1661d42ab86c9d7db5cc658e9503dbee90
...

diff -r fc770d1661d4 -r c25b7de9cc35 agda/prime.agda
--- a/agda/prime.agda	Sat Mar 13 09:38:30 2021 +0900
+++ b/agda/prime.agda	Sat Mar 13 09:50:44 2021 +0900
@@ -18,7 +18,7 @@
 open ≡-Reasoning
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
-prime-is-infinite zero pmax = {!!}
+prime-is-infinite zero pmax = pmax 1 {!!} record { isPrime = λ n lt → {!!} }
 prime-is-infinite (suc m) pmax = pmax (suc (factorial (suc m))) f>m record { isPrime = λ n lt → fact n lt } where
   factorial : (n : ℕ) → ℕ
   factorial zero = 1
@@ -30,7 +30,7 @@
   fact : (n : ℕ ) → n < (suc (factorial (suc m))) →   gcd (suc (factorial (suc m))) n ≡ 1
   fact n lt = begin
      gcd (suc (factorial (suc m))) n   ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor d ) ⟩
-     gcd ( (Dividable.factor d * n + 0) + 1)  n   ≡⟨  {!!}  ⟩
+     gcd ( (Dividable.factor d * n + 0) + 1)  n   ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (Dividable.factor d * n) 0) ⟩
      gcd ( Dividable.factor d * n + 1)  n   ≡⟨  gcdmul+1 (Dividable.factor d)  n  ⟩
      1 ∎  where
        d :  Dividable n (factorial (suc m ))