--- a/agda/gcd.agda	Sat Mar 13 00:23:23 2021 +0900
+++ b/agda/gcd.agda	Sat Mar 13 09:38:30 2021 +0900
@@ -200,3 +200,18 @@
 gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
 gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n)
 
+gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
+gcdmul+1 zero n = gcd204 n
+gcdmul+1 (suc m) n = begin
+      gcd (suc m * n + 1) n ≡⟨⟩
+      gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin
+         n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩
+         m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩
+         m * n + (n + 1)  ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩
+         m * n + (1 + n)  ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩
+         m * n + 1 + n ∎ 
+       ) ⟩
+      gcd (m * n + 1 + n) n ≡⟨ gcd2 (m * n + 1) n ⟩
+      gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
+      1 ∎ where open ≡-Reasoning
+

--- a/agda/prime.agda	Sat Mar 13 00:23:23 2021 +0900
+++ b/agda/prime.agda	Sat Mar 13 09:38:30 2021 +0900
@@ -15,24 +15,23 @@
    field
       isPrime : ( j : ℕ ) → j < i → gcd i j ≡ 1
 
-prime? : ( i : ℕ) → Dec ( Prime i )
-prime? i = {!!}
-
-not-p : (i : ℕ) → ¬ Prime i → Comp i 
-not-p = {!!}
+open ≡-Reasoning
 
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
 prime-is-infinite zero pmax = {!!}
-prime-is-infinite (suc m) pmax = {!!} where
+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
   factorial (suc n) = (suc n) * (factorial n)
-  -- gcdmul+1 : gcd (m * n + 1) n ≡ 1
-  np : (i n j : ℕ) → ((i : ℕ) → Prime i → gcd i n ≡ 1) → Prime j → gcd (i * j ) n ≡ 1
-  np = {!!}
-  pf : (j : ℕ) → j < suc (factorial (suc m)) → gcd (suc (factorial (suc m))) j ≡ 1
-  pf j j<f with prime? j
-  ... | yes y = {!!}
-  ... | no non with not-p j non 
-  ... | t = {!!}
-  
+  f>m :  suc m < suc (factorial (suc m))
+  f>m = {!!}
+  factm : (n m : ℕ ) → n < (suc (factorial m)) →  Dividable n (factorial m )
+  factm = {!!}
+  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 + 1)  n   ≡⟨  gcdmul+1 (Dividable.factor d)  n  ⟩
+     1 ∎  where
+       d :  Dividable n (factorial (suc m ))
+       d = factm n (suc m) lt