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

diff -r c25b7de9cc35 -r 1c43d0713dfc agda/prime.agda
--- a/agda/prime.agda	Sat Mar 13 09:50:44 2021 +0900
+++ b/agda/prime.agda	Sat Mar 13 15:12:18 2021 +0900
@@ -17,6 +17,20 @@
 
 open ≡-Reasoning
 
+record NonPrime ( n : ℕ ) : Set where
+   field
+      factor : ℕ
+      dividable : Dividable factor n
+
+nonPrime : ( n : ℕ ) → ¬ Prime n → NonPrime n
+nonPrime n np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
+    np1 : ( m : ℕ ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → NonPrime n
+    np1 zero mg = ⊥-elim ( np record { isPrime = λ j lt → mg j z≤n lt } ) -- zero < j , j < n
+    np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
+    ... | tri< a ¬b ¬c = {!!}
+    ... | tri≈ ¬a b ¬c = np1 m {!!}
+    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; dividable = record { factor = {!!} ; is-factor = {!!} } }
+
 prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
 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
@@ -25,13 +39,17 @@
   factorial (suc n) = (suc n) * (factorial n)
   f>m :  suc m < suc (factorial (suc m))
   f>m = {!!}
-  factm : (n m : ℕ ) → n < (suc (factorial m)) →  Dividable n (factorial m )
+  factm : (n m : ℕ ) → n < (suc 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 (suc (factorial (suc m))) n ≡⟨ {!!}  ⟩
+     -- ? ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor d ) ⟩
      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 ))
-       d = factm n (suc m) lt
+       d with <-cmp n (suc m)
+       ... | tri< a ¬b ¬c = factm n (suc m) {!!}
+       ... | tri≈ ¬a b ¬c = factm n (suc m) {!!}
+       ... | tri> ¬a ¬b c = NonPrime.dividable (nonPrime ? ? )